ETAPS 2019: 6-11 April 2019, Prague, Czech Republic

ETAPS 2019 Workshops

Workshop on Behavioural APIs (BEHAPI 2019)

APIs are software interfaces describing the services, functions or procedures offered by a software component to other components. Behavioural Types are a suite of technologies that elevate flat API descriptions to graph structures describing the intended order of usage. This permits automated analyses for correct API compositions to provide guarantees such as service compliance, deadlock freedom, dynamic adaptation in the presence of failure and load balancing. The BehAPI project aims to bring the existing prototype tools based on these technologies to mainstream programming languages and other API-based technologies.

This workshop will present ongoing research on behavioural types to assist the development of correct protocol-based systems in the large, by members of the project and by other researchers working in the area.

Organizers: Laura Bocchi, Adrian Francalanza, Hernan Melgratti, Luca Padovani, Antonio Ravara, Emilio Tuosto

Abstracts: 31 January 2019
Notification: 14 February 2019

4rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology (CREST 2019)

CREST 2019 is the third in a series of workshops addressing formal approaches to reasoning about causation in systems engineering. The topic of formally identifying the cause(s) of specific events - usually some form of failures -, and explaining why they occurred, are increasingly in the focus of several, disjoint communities.

The main objective of CREST is to bring together researchers and practitioners from industry and academia in order to enable discussions how explicit and implicit reasoning about causation is performed. 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: Georgiana Caltais, Jean Krivine

Abstracts: 27 January 2019
Papers max 15 pp eptcs.cls: 10 February 2019 (was 3 February)
 (Notification: 4 March 2019
Final versions for EPTCS: 24 May 2019

10th International workshop on Developments in Implicit Computational complExity / 6th Workshop on Foundational and Practical Aspects of Resource Analysis (DICE-FOPARA 2019)

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. Several approaches have been explored for that purpose, such as restrictions on primitive recursion and ramification, rewriting systems, linear logic, types and lambda calculus, interpretations of functional and imperative programs.

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.

DICE steering committee: Patrick Baillot, Ugo Dal Lago, Jean-Yves Marion, Simona Ronchi Della Rocca
FOPARA steering committee: Hans-Wolfgang Loidl, Marco van Eekelen

Full papers max 15 pp / extended abstracts max 5 pp eptcs.cls: 7 February 2019 (was 31 January)
Notification: 21 February 2019
Final versions: 28 February 2019

14th International Workshop on Games for Logic and Programming Languages (GaLoP 2019)

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.

This is an established ETAPS workshop, which has been running for the past 13 years.

Organiser: Pierre Clairambault

Abstracts max 1 pp (excl bibliography): 8 February 2019 (was 1 February)
Notification: 22 February 2019 

6th International Workshop on Horn Clause Verification and Synthesis (HCVS 2019)

Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses, and many recent advances in the Constraint/Logic Programming, Verification, and Automated Deduction communities have centered around efficiently solving problems presented as Horn clauses.

This workshop aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE), on the topic of Horn clause based analysis, verification and synthesis.

Horn clauses have been advocated by these communities at different times and from different perspectives, and this workshop is organized to stimulate interaction and a fruitful exchange and integration of experiences.

HCVS 2019 will host the 2nd CHC competition (CHC-COMP) which will compare state-of-the-art tools for CHC solving for performance and effectiveness on a set of publicly available benchmarks.

Organizers: Emanuele De Angelis, Grigory Fedyukovich

Regular papers max 12 pp (excl bibliography) / tool papers max 4 pp (excl bibliography) / extende abstracts max 3 pp eptcs.cls / presentation-only papers: 24 February 2019 (was 15 February)
Notification: 7 March 2019
Preproceedings versions: 15 March 2019
Final versions for EPTCS: 12 May 2019

6th International Workshop on Hybrid Systems and Biology (HSB 2019)

The workshop centres on dynamical models in biology, with an emphasis on both hybrid systems (in the classical sense, i.e., mixed continuous/discrete/stochastic systems) and hybrid approaches that combine modelling, analysis, algorithmic and experimental techniques from different areas.

Hybrid systems and approaches are essential to the understanding of complex living systems, which are characterized by stochasticity and heterogeneous (continuous and discrete) spatiotemporal scales. These methods are crucial also for the design and analysis of artificial biochemical systems (e.g., engineered bacteria or molecular machines) and of medical cyber-physical systems such as pacemakers and infusion pumps. The complexity of such models makes their formal analysis challenging, and even their simulations are frequently impractical, calling for appropriate model abstractions and scalable analysis methods.

HSB aims at bringing together researchers from different disciplines interested in applying these methods to the study of structure, dynamics, and control mechanisms of living systems.

Organizers: Milan Ceska, Nicola Paoletti

Regular papers max 15 pp (+2 pp bibliography) / tool papers max 6 pp (+2 pp bibliography) llncs.cls: 18 January 2019 (was 4 January, was 16 December 2018)
Notification: 24 February 2019 (was 15 February)
Preproceedings versions: ? (was 24 February)
Final versions for LNCS: 5 May 2019

Interactive Workshop on the Industrial Application of Verification and Testing (InterAVT 2019)

Modern verification and testing techniques are highly relevant for industrial software- intensive systems. Recent technological trends (e.g., the new dominating role of software in traditional domains like automotive and aerospace, the arrival of autonomous and “smart” systems in everyday life) only increase the need for industrial-scale robust approaches.

Nevertheless, there are still many barriers that hinder the application of modern verification and testing techniques in industrial practice.

The InterAVT workshop aims for the following workshop objectives:

  • Attract industry participants, bring researchers and practitioners together
  • Foster communication between people working on similar problems
  • Establish new links and opportunities for collaboration between participants from different backgrounds
  • Encourage report on the resulting progress at ETAPS conferences or workshops

Organizers: Stylianos Basagiannis, Goetz Botterweck, Anila Mjeda

Abstracts: 1 February 2019 (was 18 January)
Short papers 2-4 pp: 15 February 2019 (was 25 January)
Notification: ? (was 14 February)
Final versions: ? (was  28 February)

3rd Workshop on Learning in Verification (LiVe 2019)

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-tree learning 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.

Organiser: Joost-Pieter Katoen, Jan Kretinsky 

Abstracts max 2 pp llncs.cls: 15 February 2019 (was 1 February)
Notification: 1 March 2019
Final versions for informal proceedings: 10 March 2019

2nd International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2019)

Modern software systems are inherently concurrent. They consist of components running simultaneously and sharing access to resources provided by the execution platform. This leads to resource contention and potential deadlocks compromising mission- and safety-critical operations. Similar problems are observed in various kinds of software, including system, work-flow management, integration software, web services etc. Essentially, any software entity that goes beyond simply computing a certain function, necessarily has to interact and share resources with other such entities.

The intrinsic concurrent nature of such interactions is the root cause of the sheer complexity of the resulting software, which is exponential in the number of components, making complete a posteriori verification practically infeasible. An alternative approach consists in ensuring correctness by construction.

The Rigorous System Design approach is based on a formal, accountable and iterative process for deriving trustworthy and optimized implementations from models of application software, its execution platform and its external environment. A system implementation is derived from a set of appropriate high-level models by applying a sequence of semantics-preserving transformations.

Organisers: Simon Bliudze, Panagiotis Katsaros

Abstracts: (was 20 January 2019)
Full papers (regular papers / case studies / tool papers) max 12 pp eptcs.cls: 11 February  2019 (was 27 January)
Notificatiion: 1 March 2019
Preproceedings versions: 17 March 2019
Final versions for EPTCS: 28 April 2019

3rd International Workshop on Program Equivalence and Relational Reasoning (PERR 2019)

This workshop is dedicated to the formal verification of program equivalence and related relational problems. It is the 3rd in a series of meetings that bring together researchers from different areas interested in equivalence. The topic touches many aspects of formal methods: regression verification, translation validation, verified compilation, language semantics, deductive verification, (bounded) model checking, specification inference, software evolution and testing.

The goal of the workshop is to bring researchers of the different fields in touch and to stipulate an exchange of ideas leading to forging a community working on PERR. It welcomes contributions from the mentioned topics but is also open to new questions regarding program equivalence. This includes related research areas of relational reasoning like program refinement or the verification of hyper-properties, in particular of secure information flow.

Organizers: Nikos Tzevelekos, Mattias Ulbrich, Shuvendu K. Lahiri, Andrzej Murawski, O. Strichman

Abstracts 1-2 pp or papers max 15 pp: 8 February 2019 (was 1 February)
Notification: 1 March 2019

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

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: the development of programming methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern.

Organizers: Francisco Martins, Dominic Orchard

Extended abstracts 8 pp eptcs.cls (excl bibliography): 31 January 2019 (was 24 January)
Notification: 21 February 2019
Preproceedings versions: 7 March 2019

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

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. The 16th edition of QAPL will also focus on discussing the developments, challenges and results in this area covered by our workshop in its nearly 20-year history.

Organizers: Alessandro Aldini, Herbert Wiklicky

Extended abstracts max 6 pp eptcs.cls: 10 February 2019
Notification extended abstracts: 27 February 2019
Preproceedings versions of full papers: 28 February 2019
Presentation reports max 3 pp eptcs.cls: 25 February 2019
Notification presentation reports: 28 February 2019

Workshop on Security Practices for Internet of Things (SPIoT 2019)

The workshop on Security Practices for Internet of Things addresses the security issues of IoT devices from the formal and practical viewpoint. IoT devices are creeping into everyday life by promising wondrous features. However, a malicious attacker can easily exploit these devices to build botnets, lock them with ransomware, or use them as a bridgehead into less accessible networks. The objective of the SPIoT workshop is to bring together security practitioners, security-aware IoT users and formal analysis experts with the aim of sharing practices and finding guarantees about the trustworthiness of IoT devices and their use. Relevant case studies come from settings where a security flaw implies serious damage, such as in industry, safety-critical systems and healthcare.

Organizers: Saddek Bensalem, Florian Kammüller, Axel Legay, Stefano Schivo, Marielle Stoelinga

Abstracts max 2 pp llncs.cls: 25 January 2019 (was 11 January)
Notification: 15 February 2019
Final versions: 1 March 2019

6th International Workshop on Synthesis of Complex Parameters (SynCoP 2019)

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.

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). Parameterised verification is the task of verifying the correctness of this kind of systems regardless the number of their components.

Organizers: Laure Petrucci, Jaco van de Pol

Abstracts max 3 pp llncs.cls (excl bibliography): 15 February 2019 (was 14 January)
Notification: 22 February 2019
Final versions: 15 March 2019

Tutorial on Automatic Synthesis of Reactive Systems (SYNTCOMP Camp 2019)

The target audience of this short tutorial (3.5 hours) are researchers that are interested in the state of the art regarding theory and implementations of the automatic synthesis of reactive systems.

With the advent of the Reactive Synthesis Competition (SYNTCOMP), the synthesis community has made major improvements both with respect to efficient algorithms and their implementation in mature, push-button tools. On the one hand, the standard benchmark library of the competition may provide you with a potential source of interesting problems for your own research, and on the other hand reactive synthesis tools may be used as building blocks in other projects.

The tutorial will be separated into two parts: the first part will give a background on the history and the theoretical foundations of reactive synthesis and SYNTCOMP. The second part will go in-depth on one of the successful approaches and present its implementation in the tool BoSy.

Organizers: Roderick Bloem, Swen Jacobs, Guillermo A. Perez
Tutorial speakers: Leander Tentrup, Guillermo A. Perez

8th Verification Competition (VerifyThis2019)

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

The aims of the competition are:
- to bring together those interested in formal verification, and 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 by others.

The competition will offer a number of challenges presented in natural language and 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 have the input-output behavior of programs in focus. Solutions will be judged for correctness, completeness, and elegance.

Organizers: Claire Dross, Carlo A. Furia
Steering committee: Marieke Huisman , Rosemary Monahan , Peter Müller 

Problems submission deadline: 28 January 2019