ETAPS 2017

The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to Software Science.

ETAPS, established in 1998, is a confederation of five main annual conferences (ESOP, FASE, FOSSACS, POST and TACAS) accompanied by satellite workshops and other events.

The twentieth edition, ETAPS 2017, will take place in Uppsala, Sweden. This is the first time that ETAPS goes to Scandinavia.

Invited Speakers

• Dino Distefano (Facebook and Queen Mary University)
• Michael Ernst (University of Washington)
• Kim G. Larsen (Aalborg University)
• Joel Ouaknine (University of Oxford and MPI-SWS Saarbrucken)

In addition, ETAPS will feature a public lecture by Serge Abiteboul (INRIA, ENS Cachan), and invited tutorials by Veronique Cortier (CNRS, France) and Kenneth McMilllan (MSR Redmond).

Workshops

6th International Workshop on Bidirectional Transformations (BX)

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 relevant to 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 2017 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.

Organizers: Romina Eramo (University of L'Aquila, Italy), Michael Johnson (Macquarie University, Australia)

Abstracts: 20 Jan 2017
Regular papers max 15 pp, tool papers max 8 pp, short papers 4 pp, talk proposals 2 pp ceur-ws: 27 Jan 2017
Notification: 17 Feb 2017
Final versions: 1 March 2017

2nd Workshop on Causal Reasoning for Embedded and Safety-Critical Systems Technologies (CREST)

The CREST 2017 workshop is the second in a series of workshops addressing approaches to causal reasoning in the engineering of complex embedded and safety-critical systems. The main objective is to bring together researchers and practitioners from industry and academia in order to enable discussions how explicit and implicit causality reasoning is performed in the design of these systems. A further objective is to link to the foundations of causal reasoning in the philosophy of sciences and to causal reasoning performed in other areas of computer science, engineering and beyond.

Organizers: Stefan Leue (University of Konstanz, Germany), Alex Groce (Oregon State University, USA)

Abstracts: 27 Jan 2017
Papers max 15 pp eptcs.cls: 3 Feb 2017
Notification: 10 March 2017
Final versions for informal preproceedings: 24 March 2017
Final versions for EPTCS: 9 June 2017

8th Workshop on Developments in Implicit Computational complExity (DICE) and 5th Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA)

The DICE workshop explores the area of Implicit Computational Complexity (ICC), which grew out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g. Ptime, Logspace computation). It aims at studying the computational complexity of programs without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical/computational principles entailing complexity properties. The FOPARA workshop serves as a forum for presenting original research results that are relevant to the analysis of resource (e.g. time, space, energy) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions are encouraged. We also encourage papers that combine theory and practice. Given the complementarity and the synergy between these two communities, and following the successful experience of co-location of DICE-FOPARA 2015 in London at ETAPS 2015, we will hold these two workshops together at ETAPS 2017.

Organizers: Guillaume Bonfante (Universite de Lorraine, France), Georg Moser (University of Innsbruck, Austria)

Regular papers max 15 pp eptcs.cls, extended abstracts max 6 pp: 19 February 2017
Notification: 19 March 2017
Final versions: 26 March 2017

14th International Workshop on Formal Engineering Approaches to Software Components and Architectures (FESCA)

The aim of the FESCA workshop is to bring together junior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and reasoning techniques with practical benefits for software engineering. In recent years, the growing importance of functional correctness and the increased relevance of system quality properties (e.g. performance, reliability, security) have stimulated the emergence of analytical and modelling techniques for the design and development of software systems. With the increasing complexity and utilization of today's software systems, FESCA aims at addressing two research questions: (1) what role is played by the software design phase in the systematic addressing of the analytical and modelling challenges, and (2) how can formal and semi-formal techniques be effectively applied to make the issues easier to address automatically, with lower human intervention.

Organizers: Jan Kofron (Charles Univ., Czechia), Jana Tumova (KTH, Sweden)

Abstracts: 18 Jan 2017
Regular papers max 15 pp, position papers max 5 pp, talk proposals 1 p eptcs.cls: 25 Jan 2017
Notification: 27 Feb 2017
Final versions: 14 March 2017

Games for Logic and Programming Languages XII (GaLoP)

GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials. Areas of interest include Games and other interaction-based denotational and operational models; Games-based program analysis and verification; Logics for games and games for logics; Algorithmic aspects of game semantics; Categorical aspects of games semantics; Programming languages and full abstraction; Higher-order automata and Petri nets Geometry of interaction; Ludics; Epistemic game theory; Logics of dependence and independence; Computational linguistics; Games and multi-valued logics.

Organizer: Dan Ghica (University of Birmingham, UK)

Abstracts 1 p+refs: 30 Jan 2017
Notification: 20 Feb 2017

3rd Workshop on Theory and Applications of Graphs as Models (GaM)

Graphs are used as models in all areas of computer science: examples are state space graphs, control flow graphs, syntax graphs, UML-type models of all kinds, network layouts, social networks, dependency graphs, and so forth. Used to model a particular phenomenon or process, graphs are then typically analyzed to find out properties of the modelled subject, or transformed to construct other types of models. Graphs as Models combines the strengths of two pre-existing workshop series: GT-VMT (Graph Transformation and Visual Modelling Techniques) and GRAPHITE (Graph Inspection and Traversal Engineering), but also solicits research from other related areas, such as Social Network Analysis.

Organizers: Alice Miller (University of Glasgow, UK), Timo Kehrer (Politecnico di Milano, Italy)

Regular papers max 15 pp, work-in-progress papers max 15 pp, talk proposals 1-2 pp, demo proposals 1-2 pp eptcs.cls: 3 Feb 2017
Notification: 10 March 2017
Final versions: 7 April 2017

5th Workshop on Hot Issues in Security Principles and Trust (HotSpot)

This workshop is intended to be a less formal counterpart to the Principles of Security and Trust (POST) conference at ETAPS, and with an emphasis on "hot topics", both of security and of its theoretical foundations and analysis.

As the previous four issues, the edition will be part of the activities of the IFIP WG 1.7 on Theoretical Foundations of Security Analysis and Design (http://www.dsi.unive.it/IFIPWG1_7).

Like POST, the themes are:

theory of computer security;
formal specification, analysis and design of security systems;
automated reasoning for security analysis.

Organizer: Ralf Kusters (University of Trier, Germany)

Papers: 15 Jan 2017
Notification: 13 Feb 2017
Final versions for informal proceedings: 20 Feb 2017

1st Workshop on Learning in Verification (LiVe)

The success of machine learning has recently motivated researchers in formal methods to adapt the highly scalable learning methods to the verification setting, where correctness guarantees on the result are essential.

The aim of this workshop is to bring together researchers from the formal verification community that are developing approaches to exploit learning methods in verification as well as researchers from machine learning area interested in applications in verification and synthesis.

The topic includes any use of learning techniques to speed up or enhance verification, for example reinforcement learning in the analysis of complex systems, decision trees for generating invariants of programs or computing small and understandable counterexamples and controllers, or the meta-usage for predicting best tools to be applied to a verification problem.

Organizer: Jan Kretinsky (Technische Univ. Munchen, Germany)

Abstracts: 3 Feb 2017
Notification: 21 Feb 2017
Final versions of abstracts for informal proceedings: 1 March 2017

2nd Workshop on Models for Formal Analysis of Real Systems (MARS)

Specification formalisms and modelling techniques have often been developed with formal analysis and formal verification in mind. To demonstrate applicability, tiny case studies are typically presented in research papers. To show that a developed approach actually scales to real systems, large case studies are essential. The process of developing a detailed and accurate model usually takes a considerable amount of time, often months to years.

This workshop emphasises modelling. In particular, we invite papers that present full models of real systems, which may lay the basis for future comparison and analysis. The workshop brings together researchers from different communities facing real systems and developing formal models thereof, especially in areas where large models occur, such as networked or cyber-physical systems.

Organizers: Holger Hermanns (Univ. des Saarlandes, Germany), Peter Hofner (CSIRO, Australia)

Papers max 12 pp eptcs.cls: 13 Jan 2017
Notification: 13 Feb 2017
Final versions: 27 Feb 2017

11th International Workshop on Model-Based Testing (MBT)

The workshop is devoted to model-based testing of both software and hardware. Model-based testing uses models describing the required behavior of the system under consideration to guide such efforts as test selection and test results evaluation. Testing validates the real system behavior against models and checks that the implementation conforms to them, but is capable also to find errors in the models themselves.

Model-based testing has gained attention with the popularization of models in software/hardware design and development. Of particular importance are formal models with precise semantics, such as state-based formalisms, algebraic specifications, or other mathematical descriptions of possible system behavior. Testing with such models allows one to detect subtle bugs and at the same time to measure the degree of the product's conformance with the model. Recently model-based testing get particular importance in such domains as security testing and testing of hybrid systems due to their inherent complexity.

Techniques to support model-based testing are drawn from diverse areas, like deductive verification, model checking, constraint solving, control and data flow analysis, grammar analysis, Markov processes, etc.

The intent of this workshop is to bring together researchers and users of model-based testing techniques and tools to discuss the state of the art in theory, applications, tools, and industrialization of model-based testing and related domains.

Organizers: Holger Schlingloff (Humboldt-Universitat Berlin, Germany), Alexandre Petrenko (CRIM, Canada)

Research papers max 15 pp, industrial experience papers max 15 pp, industrial presentations abstracts only eptcs.cls: 31 Jan 2017
Notification: 21 Feb 2017
Final versions: 28 Feb 2017

10th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES)

Applications today are built using numerous interacting services; soon off-the-shelf CPUs will host thousands of cores, and sensor networks will be composed from a large number of processing units. Many applications need to make effective use of thousands of computing nodes. At some level of granularity, computation in such systems is inherently concurrent and communication-centred. PLACES aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming in the near future, the development of programming methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern.

Organizer: Vasco T. Vasconcelos (University of Lisbon, Portugal)

Abstracts: 29 Jan 2017
Extended abstracts max 6 pp eptcs.cls: 5 Feb 2017
Notification: 5 March 2017
FInal versions: 17 March 2017

5th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL)

Quantitative aspects of computation refer to the use of physical quantities (time, bandwidth, etc.) as well as mathematical quantities (for example, probabilities) for the characterisation of the behaviour and for determining the properties of systems. Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of the QAPL workshop series is to discuss the explicit use of time and probability and general quantities either directly in the model or as a tool for the analysis or synthesis of systems.

Organizers: Erik de Vink (Eindhoven University of Technology, The Netherlands), Herbert Wiklicky (Imperial College London, UK)

Regular papers max 12 pp+refs eptcs.cls: 5 Feb 2017
Notification: 10 March 2017
Final versions for informal preproceedings: 25 March 2017
FInal versions for EPTCS: tba

Presentation reports max 4 pp eptcs.cls: 12 March 2017
Notification: 15 March 2017

2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR)

Hybrid systems are complex dynamical systems that combine discrete and continuous components. Reachability questions, regarding whether a system can run into a certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems. The SNR workshop aims to catalyze work on the interface of symbolic and numerical methods for reachability analysis. In particular, the scope of the workshop includes, but is not restricted to, the following topics: verification of hybrid systems, flow-pipe construction, symbolic representation of regions in reachability analysis algorithms, abstraction techniques for hybrid systems and numerical programs, trajectory generation from symbolic paths, counterexample computation, reliable integration, decision procedures over real numbers, logics to reason about hybrid systems, reachability analysis for planning and synthesis, domain specific approaches in biology, robotics, etc.

Organizers: Erika Abraham (RWTH Aachen University, Germany), Sergiy Bogomolov (Australian National University, Australia)

Abstracts: 27 Jan 2017
Regular papers max 15 pp+refs, short papers max 6 pp+refs, work-in-progress papers max 6 pp+refs eptcs.cls: 3 Feb 2017
Notification: 10 March 2017
Final versions: 24 March 2017

4th International Workshop on Synthesis of Complex Parameters (SynCoP) and 3rd International Workshop on Parameterized Verification (PV)

SynCoP aims at bringing together researchers working on verification and parameter synthesis for systems with discrete or continuous parameters, in which the parameters influence the behavior of the system in ways that are complex and difficult to predict. Such problems may arise for real-time, hybrid or probabilistic systems in a large variety of application domains. The parameters can be continuous (e.g., timing, probabilities, costs) or discrete (e.g., number of processes). The goal can be to identify suitable parameters to achieve desired behavior, or to verify the behavior for a given range of parameter values. PV aims at bringing together researchers working on Parameterized Verification. Systems composed of a finite but possibly arbitrary number of identical components occur everywhere from hardware design (e.g. cache coherence protocols) to distributed applications (e.g. client-server applications). Parameterized verification is the task of verifying the correctness of this kind of systems regardless the number of their components. The workshop is organized as a series of tutorial and invited talks, and covers

Specifications in automata and logic, term and graph rewriting, Petri nets, process algebra, etc.
Validation methods via assertional and regular model checking, reachability and coverability decision procedures, abstractions, theorem proving, constraint solving, etc.
Applications to hardware design, cache coherence protocols, security and communication protocols, multithreaded and concurrent programs, programs with relaxed memory models, mobile, distributed, and IoT systems, database languages and systems, biological systems, etc.

Organizer: Peter Habermehl (University Paris Diderot, Paris 7, France), Giorgio Delzanno (Universita di Genova, Italy)

6th VerifyThis Verification Competition

VerifyThis is a series of program verification competitions held earlier at FoVeOOS2011, FM2012, Dagstuhl (April 2014), ETAPS 2015 and 2016.

Its aims are:
to bring together those interested in formal verification,
to provide an engaging, hands-on, and fun opportunity for discussion,
to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated.

The competition will offer a number of challenges presented in natural language or pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.

There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will focus on the input-output behavior of programs, yet it is at the discretion of participants to treat only aspects of requirements. Solutions will be judged for correctness, completeness, degree of automation, and elegance.

Organizers: Marieke Huisman (Universiteit Twente, The Netherlands), Rosemary Monahan (NUI Maynooth, Ireland), Peter Muller (ETH Zurich, Switzerland)

5th International Workshop on Verification and Program Transformation (VPT)

The workshop aims at bringing together researchers working in the fields of Program Verification and Program Transformation. Recent research in these areas has shown a great potential for beneficial interactions. On one hand, methods and tools for Program Transformation such as partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success for the verification of infinite state and parameterized systems. On the other hand, model checking, abstract interpretation, SAT and SMT solvers, and automated theorem provers have been used to enhance program transformation techniques. Moreover, the formal certification of tools, such as compilers and automated refactoring tools, has recently attracted considerable interest and posed new challenges. The workshop will also provide a forum where researchers from these fields may interact and foster new developments.

Organizers: Maurizio Proietti (IASI CNR, Italy), Alexei Lisitsa (Univ. of Liverpool), Andrei P. Nemytykh (Program Systems Institute, Russia)

Abstracts: 31 Jan 2017
Papers max 15 pp eptcs.cls: 6 Feb 2017
Notification: 8 March 2017
Final versions for informal preproceedings: 31 March 2017
Final versions for EPTCS: tba

Organizers

General chair

• Parosh Aziz Abdulla

Organizing Committee Members

• Wang Yi
• Bjorn Victor
• Yunyun Zhu

Tutorials and workshops chairs

Konstantinos Sagonas, Mohamed Faouzi Atig

Publicity chairs

• Andreina Francisco
• Kaj Lampka
• Tjark Weber

Web chair

• Philipp Rummer

Host institution

• Department of Information Technology, Uppsala University