[TYPES/announce] [CFP] Bx 2019: 8th International Workshop on Bidirectional Transformations (Deadline: Feb. 19)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Bx 2019: 8th International Workshop on Bidirectional Transformations * http://bx-community.wikidot.com/bx2019:home * Saint Joseph’s University, Philadelphia, PA, USA * exact date TBD (some day during 3–7 June 2019) * as part of Philadelphia Logic Week (PLW) 2019 https://sites.sju.edu/plw/ Bidirectional transformations (bx) are a mechanism for maintaining the consistency of at least two related sources of information. Such sources can be relational databases, software models and code, or any other document following standard or ad-hoc formats. Bx are an emerging topic in a wide range of research areas, with prominent presence at top conferences in several different fields (namely databases, programming languages, software engineering, and graph transformation), but with results in one field often getting limited exposure in the others. Bx 2019 is a dedicated venue for bx in all relevant fields, and is part of a workshop series that was created in order to promote cross-disciplinary research and awareness in the area. As such, since its beginning in 2012, the workshop has rotated between venues in different fields. Important Dates === - Abstract submission: 12 Feb 2019 (AoE) - Paper submission:19 Feb 2019 (AoE) - Author notification: 8 Apr 2019 - Camera-ready version: around 1 May 2019 - Workshop: some day during 3–7 June 2019 Aims and Topics === The aim of the workshop is to bring together researchers and practitioners, established and new, interested in bx from different perspectives, including but not limited to: - bidirectional programming languages and frameworks - data and model synchronization - view updating - inter-model consistency analysis and repair - data/schema (or model/metamodel) co-evolution - coupled software/model transformations - inversion of transformations and data exchange mappings - domain-specific languages for bx - analysis and classification of requirements for bx - bridging the gap between formal concepts and application scenarios - analysis of efficiency of transformation algorithms and benchmarks - survey and comparison of bx technologies - case studies and tool support Submission Guidelines = Papers must follow the CEUR one-column style available at http://ceur-ws.org/Vol-XXX/samplestyles/ and must be submitted via EasyChair: https://www.easychair.org/conferences/?conf=bx2019 Five categories of submissions are considered: * Full Research Papers (up to 15 pages) - in-depth presentations of novel concepts and results - applications of bx to new domains - survey papers providing novel comparisons between existing bx technologies and approaches case studies * Tool Papers (up to 8 pages) - guideline papers presenting best practices for employing a specific bx approach (with a specific tool) - presentation of new tools or substantial improvements to existing ones - qualitative and/or quantitative comparisons of applying different bx approaches and tools * Experience Report (up to 8 pages) - sharing experiences and lessons learned with bx tools/frameworks/languages - how bx is used in (research/industrial/educational) projects * Extended Abstracts (up to 4 pages) - work in progress - small focused contributions - position papers and research perspectives - critical questions and challenges for bx * Talk Proposals (up to 2 pages) - proposed lectures about topics of interest for bx - existing work representing relevant contributions for bx - promising contributions that are not mature enough to be proposed as papers of the other categories The bibliography is excluded from the page limits. All papers are expected to be self-contained and well-written. Tool papers are not expected to present novel scientific results, but to document artifacts of interest and share bx experience/best practices with the community. Experience papers are expected to report on lessons learnt from applying bx approaches, languages, tools, and theories to practical application case studies. Extended abstracts should primarily provoke interesting discussion at the workshop and will not be held to the same standard of maturity as regular papers. Talk proposals are expected to present work that is of particular interest to the community and worth a talk slot at the workshop. We strongly encourage authors to ensure that any (variants of) examples are present in the bx example repository at the time of submission, and for tool papers, to allow for reproducibility with minimal effort, either via a virtual machine (e.g., via Share - http://share20.eu) or a dedicated website with relevant artifacts and tool access. All papers will be peer-reviewed by at least three members of the programme committee. If a paper is accepted, one author of the paper is expected to
[TYPES/announce] Postdoc position: Symbolic tools for the formal verification of cryptographic protocols
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] A 12-month position for post-doctoral research on Symbolic tools for the formal verification of cryptographic protocols is available at the Inria Nancy / LORIA research center within the Inria project team PESTO: Proof techniques for security protocols [1] as part of the ERC Grant SPOOC: Automated Security Proofs of Cryptographic Protocols [2] Security protocols are distributed programs that aim at ensuring security properties, such as confidentiality, authentication or anonymity, by the means of cryptography. Such protocols are widely deployed, e.g., for electronic commerce on the Internet, in banking networks, mobile phones and more recently electronic elections. As properties need to be ensured, even if the protocol is executed over untrusted networks (such as the Internet), these protocols have shown extremely difficult to get right. Formal methods have shown very useful to detect errors and ensure their correctness. One generally distinguishes two families of security properties: trace properties and observational equivalence properties. Trace properties verify a predicate on a given trace and are typically used to express authentication properties. Observational equivalence expresses that an adversary cannot distinguish two situations and is used to model anonymity and strong confidentiality properties. The Tamarin prover [3] is a state-of-the art protocol verification tool which has recently been extended to verify equivalence properties in addition to trace properties. SAPIC [4] allows protocols to be specified in a high-level protocol specification language, an extension of the applied pi-calculus, and uses the Tamarin prover as a backend by compiling the language into multi-set rewrite rules, the input format of Tamarin. Tamarin and SAPIC have been successfully used to verify standards such as TLS 1.3 and 5G AKA as well as industrial protocols such as OPC UA. The objective of this postdoc is to contribute to the development of the SAPIC/Tamarin toolchain, work on extensions and use the tool(s) to analyse particular classes of protocols. Successful candidates must have defended a PhD in computer science, or expect to defend their PhD before taking up the position. Expected qualifications are: - solid knowledge of logic, proofs and/or formal verification techniques, - solid programming experience, ideally with functional programming in OCAML or Haskell. Security knowledge is not required, but a plus. Contacts: Jannik Dreier (jannik.dre...@loria.fr) Steve Kremer (steve.kre...@loria.fr) Duration: 12 months (possibility to extend for another 12 months) Starting date: September 1, 2019 (earlier date negociable) The position is located at the Inria Nancy / LORIA research center in Nancy, France, with over 430 researchers, engineers and technicians. Nancy is a young (more than 45,000 students) city in eastern France with a rich cultural life and a high quality of life. It is famous for its Unesco World Heritage Site "Place Stanislas". Paris is only 1h30 by TGV, Luxembourg, Germany and the Vosges mountains less than 1h30 by car. Applications, including - a motivation letter including your scientific and career projects, - a CV describing your research activities (max. 2 pages), - a short description of your best contributions (max. 1 page for max. 3 contributions including theoretical research, implementation or industry transfer), - your two best publications, - if you have not defended yet, the list of expected members of your PhD committee and the expected date of defense, should be sent to the the addresses indicated above as two pdf files (one for the publications, the other for the other documents). Additionally, at least one recommendation letter from your PhD advisor(s), and up to two additional letters of recommendation should be sent directly by their authors to the email addresses indicated above. Applications should be received by June 30, 2019, but applications received later may still be considered. Informal enquiries concerning the position are welcome. [1] https://team.inria.fr/pesto/ [2] http://homepages.loria.fr/skremer/spooc/ [3] http://tamarin-prover.github.io/ [4] http://sapic.gforge.inria.fr/
