ETAPS 2020 Workshops

Workshop Schedule

You can view the detailed workshop programs by clicking the workshop name in the schedule below.text

15th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2020)

In more than a decade of research, it has been established that a wide variety of state-based dynamical systems, like transition systems, automata (including weighted and probabilistic variants), Markov chains, and game-based systems, can be treated uniformly as coalgebras. Coalgebra has developed into a field of its own interest presenting a deep mathematical foundation, a growing field of applications, and interactions with various other fields such as reactive and interactive system theory, object-oriented and concurrent programming, formal system specification, modal and description logics, artificial intelligence, dynamical systems, control systems, category theory, algebra, analysis, etc. The aim of the workshop is to bring together researchers with a common interest in the theory of coalgebras, their logics, and their applications.

Organisers: Daniela Petrisan (Université de Paris, IRIF), Jurriaan Rot (University College London and Radboud University Nijmegen)

Submission abstracts: January 15, 2020
Submission regular papers: January 17, 2020
Notification regular papers: February 17, 2020
Camera-ready copy: February 28, 2020
Submission short contributions: March 04, 2020
Notification short contributions: March 04, 2020

5th Workshop on Formal Reasoning about Causation, Responsibility, & Explanations in Science & Technology (CREST 2020)

The CREST 2020 workshop is the fifth 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.

Organisers: Alexander Pretschner (TU Munich), David Landsberg (University College London)

Submission: January 25, 2020
Notification: February 29, 2020
Camera-ready (post-proceedings): June 1, 2020

Games for Logic and Programming Languages XV (GaLoP XV)

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;
  -Game-based program analysis and verification;
  -Logics for games and games for logics;
  -Algorithmic aspects of game semantics;
  -Categorical aspects of game 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.

Organiser: Dan R. Ghica (University of Birmingham)

Submission: February 7, 2020
Notification: February 28, 2020

7th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2020)

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.

Organisers: Fabio Fioravanti (Università "G. D'Annunzio" di Chieti-Pescara)

Submission: February 26, 2020
Notification: March 25, 2020
Camera-ready: April 1, 2020

2nd Interactive Workshop on the Industrial Application of Verification and Testing (InterAVT 2020)

Modern verification and testing techniques are highly relevant for industrial software- intensive systems. Recent technological trends only increase the need for industrial-scale robust approaches. Nevertheless, there are still many barriers that hinder their application in industrial practice, e.g.,
  - Industrial scale and complexity of “real” systems
  - Usability/feasibility of formal techniques in practice
  - New system paradigms make systems harder to analyze/verify/test (e.g., autonomous systems, machine learning)
Many of these challenges can only be tackled with increased communication and collaboration between researchers and practitioners. Consequently, this workshop aims to:
  - Attract industry participants, bring researchers and practitioners together
  - Foster communication between people working on similar problems
  - Establish new opportunities for collaboration between participants from different backgrounds
  - Encourage report on the resulting progress at ETAPS conferences or workshops

Organisers: Stylianos Basagiannis (United Technology Research Center), Goetz Botterweck (Lero)

Submission: February 21, 2020
Notification: March 13, 2020
Camera-ready: April 3, 2020

4th Workshop on Learning in Verification (LiVe 2020)

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 general topic of machine learning in verification includes, for instance, the use of learning techniques (e.g. reinforcement learning) for speeding up verification (e.g. rigorous analysis of complex systems combining non-determinism, stochasticity, timing etc.); the use of machine learning data structures and algorithms (e.g. decision trees) for enhancing results of verification (e.g. generating simple invariants of programs generating small controllers of systems); verification of machine-learning artefacts (e.g. verification of neural networks); or meta-usage of machine learning (e.g. to predict the best tools to be applied to a verification problem).

Organisers: Jan Kretinsky (TU Munich), Joost-Pieter Katoen (RWTH Aachen)

Submission: February 15, 2020
Notification: March 1, 2020
Camera-ready (informal pre-proceedings): March 10, 2020

4th Workshop on Models for Formal Analysis of Real Systems (MARS 2020)

The MARS workshops aim at demonstrating the applicability of formal methods on real systems and, thus, focus on large case studies rather than tiny examples typically presented in research papers. The MARS workshops emphasise modelling aspects, knowing that the development of detailed and accurate models usually takes considerable effort, often months to years.
The MARS workshops bring together researchers from different communities facing real systems and developing formal models thereof, especially in areas where large models occur, such as networks, cyber-physical systems, or hardware/software codesign. The goals of the workshops are to present models written using different specification formalisms, to consider different modelling approaches, discuss pros and cons for each of them with formal analysis and formal verification in mind.
The formal models presented during the MARS workshops are archived in the MARS repository (http://mars-workshop.org/repository.html), a growing, diverse collection of realistic benchmarks, provided in machine-readable form and licensed under Creative Commons. The existence of the MARS repository is a unique feature that makes MARS papers available to the wider community so that others can reproduce experiments, perform further analyses and try the same case studies with different formal methods.

Organisers: Ansgar Fehnker (University of Twente), Hubert Garavel (INRIA)

Submission: January 12, 2020
Notification: February 23, 2020
Camera-ready: March 15, 2020

3rd International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2020)

The intrinsic concurrent nature of interactions among components of modern software systems is the root cause of their sheer complexity, making complete a posteriori verification practically infeasible. An alternative approach consists in ensuring correctness by construction.
The term "Rigorous System Design" (RSD) denotes the design approach that is based on a formal, accountable and iterative process for deriving trustworthy and optimised implementations from models of application software, its execution platform and its external environment. Ideally, a system implementation is derived from a set of appropriate high-level models by applying a sequence of semantics-preserving transformations.
The ambition of MeTRiD is to promote the use of formal methods, in general, and the RSD approach, in particular, in the industrial applications and, reciprocally, bring the attention of the academic community to such industrial applications in order to develop realistic case-studies and guide the evolution of tools.

Organisers: Panagiotis Katsaros (Aristotle University of Thessaloniki), Marius Bozga (Universite Grenoble Alpes)

8th Workshop on Mathematically Structured Functional Programming (MSFP 2020)

Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control.

Organisers: Max S. New (Northeastern University), Sam Lindley (University of Edinburgh)

Submission abstracts: January 9, 2020
Submission regular papers: January 16, 2020
Notification: February 27, 2020
Camera-ready: March 26, 2020

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

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.

Organisers: Stephanie Balzer (Carnegie Mellon University), Luca Padovani (University of Torino)

Submission: January 24, 2020
Notification: February 28, 2020
Camera-ready copy: March 13, 2020

Rust Verify (RW 2020)

Rust is a new programming language that is becoming increasingly popular for writing systems code. This workshop aims to bring together language designers, application developers and formal verification tool builders, to foster a community of those interested in developing verified Rust programs.

Organisers: Rajeev Joshi (Amazon), Nicholas Matsakis (Mozilla), Peter Müller (ETH Zurich)

Submission: February 7, 2020
Notification: February 17, 2020

7th International Workshop on Synthesis of Complex Parameters (SynCoP 2020)

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.

Organiser: Nathalie Bertrand (INRIA), Benoît Delahaye (University of Nantes)

Workshop on Trends, Extensions, Applications and Semantics of Logic Programming (TEASE-LP)

Logic programming is a framework for expressing programs, propositions and relations as Horn clause theories, and for automatic inference in these theories. Horn clause theories are famous for its well-understood declarative semantics, in which models of logic programs are given inductively or coinductively. At the same time, Horn clauses give rise to efficient inference procedures, usually involving resolution. Logic programming found applications in type inference, verification, and AI. While logic programming was originally conceived for describing simple propositional facts, it was extended to account for much more complex theories. This includes first-order theories, higher-order theories, inductive and coinductive data, and stochastic/probabilistic theories.
The aim of this workshop is to bring together researchers that work on extensions of logic programming and inference methods, and to foster an exchange of methods and applications that have emerged in different communities.

Organisers: Henning Basold (ENS Lyon), Ekaterina Komendantskaya (Heriot-Watt University)

Submission abstracts: February 26, 2020
Notification: March 25, 2020
Camera-ready: April 1, 2020

VerifyThis Verification Competition 2020 (VerifyThis 2020)

VerifyThis is a series of program verification competitions held earlier at FoVeOOS2011, FM2012, Dagstuhl (April 2014), ETAPS 2015-2019. 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.

Organisers: Marieke Huisman (University of Twente), Rosemary Monahan (NUI Maynooth), Peter Müller (ETH Zurich), Mattias Ulbrich (Karlsruhe Institute of Technology)

8th International Workshop on Verification and Program Transformation (VPT 2020)

The aim of the workshop is to bring together researchers working in the fields of Program Verification and Program Transformation. There is great potential for beneficial interactions between these two fields because:
  (i) methods and tools developed in the field of Program Transformation such as partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success in the field of the verification of infinite-state systems and parameterized systems, and
  (ii) model checking, abstract interpretation, SAT and SMT solving and automated theorem proving have been used to enhance program transformation techniques. Moreover, the formal certification of program transformation tools, such as refactoring tools and compilers, has recently attracted considerable interest and posed major challenges.

Organisers: Alexei Lisitsa (University of Liverpool), Andrei P. Nemytykh (Program Systems Institute of RAS)

Submission abstracts (optional): January 13, 2020
Submission regular papers: January 20, 2020
Extended abstracts & presentations: February 10, 2020
Notification: April 9, 2020
Camera-ready (informal pre-proceedings): March 23, 2020

25th International Workshop on Algebraic Deveolment Techniques (WADT 2020)

The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as a formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect- oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends.

Organiser: Markus Roggenbach (University of Swansea)

Submission abstracts: February 14, 2020
Notification: February 24, 2020
Camera-ready (abstracts): April 3, 2020
Submission full papers (post proceedings): May 19, 2020
Notification full papers: June 26, 2020
Camera-ready (full papers): July 17, 2020

13th International Workshop on Rewriting Logic and its Applications (WRLA 2020)

Rewriting is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application domains. It also has good properties as a metalogical framework for representing logics. Several successful languages based on rewriting (ASF+SDF, CafeOBJ, ELAN,Maude) have been designed and implemented. The aim of WRLA is to bring together researchers with a common interest in rewriting and its applications, and to give them the opportunity to present their recent work, discuss future research directions, and exchange ideas.

Organisers: Narciso Martí-Oliet , Santiago Escobar

Submission: January 26, 2020
Notification: February 10, 2020
Camera-ready: March 1, 2020