ETAPS 2022 Workshops

General Information about ETAPS 2022 Workshops

Location: All workshops will be held in the computer-science building at TU Munich in Garching.

For rooms, dates, and Zoom links, please check the programme.

Registration: The workshop registration includes meeting rooms, coffee breaks, and lunches. The coffee breaks are shared coffee breaks on the Magistrale (ground floor) in the building.

Schedule: Coffee breaks and lunch are during the following times: 10:00 - 10:30, 12:30 - 14:00, 16:00 - 16:30.

If you do not find what you are looking for, please send me an e-mail (Dirk Beyer).

16th Workshop on Coalgebraic Methods in Computer Science, CMCS 2022

Date: Sat-Sun, April 2-3

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.

Organizers Helle Hvid Hansen (University of Groningen, Netherlands), Fabio Zanasi (University College London, UK)

Abstracts of regular papers: was 24 Jan. 2022 31 Jan 2022
Regular papers max 18 pp + refs llncs.cls: was 27 Jan. 2022 3 Feb. 2022
Notification of regular papers: 28 Feb. 2022
Final versions: 14 March 2022
Short contributions max 2 pp: 2 March 2022
Notification of short contributions: 8 March 2022

3rd Workshop on Cooperative Software Verification, COOP 2022

Date: Sun, April 3

Cooperative software verification aims at increasing the effectiveness of verification by having different verifiers cooperate on a verification task. Cooperation might take the form of black-box combinations, exchanging information via externally stored data, or of tightly integrated white-box combinations. Such combinations might include different specific verification techniques as well as combinations of verification with testing or other means of software analysis. Possible topics are

Combining testing and verification
Combining theorem proving and testing or verification
Selection of components in a cooperative verification
Interfaces and exchange formats
Modularization of existing approaches
Portfolio approaches
Languages for specifying cooperation

We welcome all sorts of talks, ranging from new ideas over work in progress to mature (possibly already published) approaches. The main objective of the workshop is to discuss ideas for cooperative verification.

Organizers Dirk Beyer (LMU Munich, Germany), Heike Wehrheim (Universität Oldenburg, Germany)

Abstracts: 15 Feb. 2022
Notification: 1 March 2022

9th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2022

Date: Sun, April 3 (joint with VPT)

Most program verification and synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the automated deduction, constraint/logic programming and verification communities have centered around efficiently solving problems presented as Horn clauses.

This workshop aims to bring together researchers working in the communities of automated deduction (e.g., CADE), constraint/logic programming (e.g., ICLP and CP) and program verification community (e.g., CAV, TACAS, and VMCAI) on the topic of Horn clause based analysis, verification and synthesis.

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

Organizer Fabio Fioravanti (Università "G. D'Annunzio" di Chieti-Pescara, Italy)

Regular papers max 12 pp + refs, tool papers max 4 pp, extended abstracts max 3 pp eptcs.cls / presentation-only papers: was 31 Jan. 2022 13 Feb. 2022
Notification: was 28 Feb. 2022 3 March 2022

6th Workshop on Learning in Verification, LiVe 2022

Date: Sat, April 2

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).

Organizer Jan Křetínský (TU Munich, Germany)

Extended abtracts 2 pp llncs.cls: 15 Feb. 2022
Notification: 1 March 2022
Final versions for informal proceedings: 10 March 2022

5th Workshop on Models for Formal Analysis of Real Systems, MARS 2022

Date: Sat, April 2

Specification formalisms and modelling techniques have often been developed with formal analysis and formal verification in mind. To show applicability, toy examples or tiny case studies are typically presented in research papers. Since the theory needs to be developed, this approach is reasonable. However, to show that a developed approach actually scales to real systems, large case studies are essential.

When showing results on a formal analysis of large-scale case studies in a scientific paper, details of the model have to be skipped due to lack of space. Often, the lessons learnt from modelling are also not discussed since they are not within the main focus of the paper.

The workshop aims at discussing exactly these unmentioned lessons. Examples are:

Which formalism is chosen, and why?
Which abstractions have to be made and why?
How are important characteristics of the system modelled?
Were there any complications while modelling the system?
Which measures were taken to guarantee the accuracy of the model?

Organizers Clemens Dubslaff (TU Dresden, Germany), Bas Luttik (TU Eindhoven, Netherlands)

Papers max 12 pp + refs eptcs.cls: 10 Jan. 2022
Notification: 14 Feb. 2022
Final versions: 28 Feb. 2022

ETAPS Mentoring Workshop, EMW 2022

Date: Sun, April 3

The ETAPS Mentoring Workshop (EMW) is intended to provide students with advice on research, career, and life in the fields of Computing that are covered by the ETAPS conference. Researchers of different academic seniority will give inspirational talks about their own path, choices, insights, experiences, and other advice to pass on. There will also be a panel discussion about various aspects of research and career. In addition, the workshop aims to enable opportunities for students and seniors to connect during ETAPS also outside the mentoring workshop.

Organizers Wolfgang Ahrendt (Chalmers Univ. of Technology, Sweden), Gidon Ernst (LMU Munich, Germany), Caterina Urban (Inria, ENS, France)

9th Workshop on Mathematically Structured Functional Programming, MSFP 2022

Date: Sat, April 2

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.

Organizers Max S. New (University of Michigan, USA), Jeremy Gibbons (University of Oxford, UK)

Abstracts: 16 Dec. 2021
Papers max 15 pp, extended abstracts max 2 pp eptcs.cls: 23 Dec. 2021
Notification: 27 Jan. 2021
Final versions: 24 Feb. 2021

13th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2022

Date: Sun, April 3

The increasingly concurrent and parallel landscape of hardware and software infrastructures demands the exploration and understanding of a wide variety of foundational and practical ideas. The workshop offers a forum for researchers from different fields to exchange new ideas about these challenges to modern and future programming, where concurrency and distribution are the norm rather than a marginal concern. Submissions are invited in the general area of programming language approaches to concurrency, communication and distribution, ranging from foundational issues, through language implementations, to applications and case studies.

Relevant topics include, but are not limited to:

Design and implementation of programming languages with first-class concurrency and communication primitives
Models for concurrent and distributed systems, such as process algebra and automata, and their mechanisation in proof assistants
Behavioural types, including session types
Concurrent data types, objects and actors
Verification and program analysis methods for safe and secure concur
Interface and contract languages for communication and distribution
Applications to microservices, sensor networks, scientific computing, HPC, blockchains

Organizers Rumyana Neykova (Brunel University, UK), Marco Carbone (ITU Copenhagen, Denmark)

Papers max 8 pp + refs eptcs.cls: was 4 Feb. 2022 11 Feb. 2022
Notification: 28 Feb. 2022
Final versions: 11 March 2022

3rd Workshop on Quantitative Aspects of Variant-rich Systems, QAVS 2022

Date: Sun, April 3

Families of systems arise naturally in software and hardware: whenever there are configuration parameters, optional features, or updating functionalities, the system can be described by a collection of variants. The often huge number of variants render their design, modeling, and analysis challenging tasks. Due to the rising impact of co-adaptive and autonomous cyber-physical systems, quantitative aspects such as probability of failure, energy consumption, or numerical parameter values gain more and more attention in configurable systems analysis. The main goal of this workshop is to bring researchers together, presenting the different approaches to deal with non-functional properties of variant-rich systems.

Organizers Clemens Dubslaff (TU Dresden, Germany), Maurice ter Beek (CNR ISTI, Italy)

Regular papers max 12 pp + refs, short papers max 6 pp + refs, presentation-only papers max 2 pp eptcs.cls: was 10 Jan. 2022 24 Jan. 2022
Notification: was 14 Feb. 2022 28 Feb 2022
Final versions: was 28 Feb. 2022 14 March 2022

1st Workshop on Reproducibility and Replication of Research Results, RRRR 2022

Date: Sat, April 2

The RRRR workshop provides a forum to present novel approaches to foster reproducibility of research results, and replication studies of existing work, in the broad area of formal methods research. Its goal is to spread the word on best practices, and reward the work invested in replicating results. Where reproducible research can be independently confirmed by third parties using artifacts provided by the original authors, replicating a result means to independently obtain it using new measurements, data, or implementations. RRRR will improve the knowledge transfer between the many separate initiatives—like artifact evaluations and tool competitions—that today support reproducibility, and provide a venue to formally publish replication studies, recognising their immense benefit to the scientific community and the hard work involved.

Organizers Dirk Beyer (LMU Munich, Germany), Arnd Hartmanns (Universiteit Twente, Netherlands)

Short papers 6 pp + refs llncs.cls: was 1 Feb 2022 24 Feb 2022
Extended abstracts 2 pp llncs.cls: was 15 Feb 2022 24 Feb 2022
Notification: was 1 March 2022 3 March 2022
Final versions for preproceedings: was 10 March 2022 17 March 2022

2nd Rust Verification Workshop, RW 2022

Date: Sun, April 3

Rust is a new programming language for writing performant code with strong type and memory safety guarantees. It is now considered a serious alternative to C and C++ for systems programming, because it provides high-level abstractions but without the cost of garbage collection. Given the growing popularity of Rust, and given that bugs in systems programs can be costly, there is growing interest in the program verification community for building program verifiers for Rust. In this workshop, we aim to bring together language designers, application developers and formal verification tool builders, to exchange ideas and build collaborations around developing verified Rust programs.

Organizers Rajeev Joshi (Amazon Web Services, USA), Nicholas Matsakis (Amazon Web Services, USA), Peter Müller (ETH Zürich, Switzerland)

Talk and demo proposals max 2 pp: 14 Jan. 2022
Notification: 7 Feb. 2022

7th International Workshop on Synthesis of Complex Parameters, SynCoP 2022

Date: Sat, April 2

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.

Organizers Benoit Delahaye (University of Nantes, France), Nathalie Bertrand (INRIA, France)

VerifyThis Verification Competition 2022

Date: Sat-Sun, April 2-3

VerifyThis is a series of program verification competitions held earlier at FoVeOOS 2011, FM 2012, Dagstuhl (2014), ETAPS 2015-2019 and 2021.

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 Marie Farrell (University of Maynooth, Ireland), Marieke Huisman (University of Twente, Netherlands), Peter Lammich (University of Twente), Rosemary Monahan (Maynooth University, Ireland), Peter Müller (ETH Zürich, Switzerland), Mattias Ulbrich (KIT, Germany)

10th International Workshop on Verification and Program Transformation, VPT 2022

Date: Sat, April 2 Sun, April 3 (joint with HCVS)

The aim of the workshop is to bring together researchers working in the fields of Program Verification and Program Transformation. There is a great potential for beneficial interactions between these two fields because:

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

Organizers Alexei P. Lisitsa (University of Liverpool, UK), Andrey P. Nemytykh (ISP RAS, Russia)

Abstracts of regular papers: was 10 Jan. 2022
Regular papers max 15 pp eptcs.cls (incl refs): was 17 Jan. 2022 was 31 Jan. 2022 13 Feb. 2022
Extended abstracts and presentation-only papers: was 31 Jan. 2022 13 Feb. 2022
Notification: was 14 Feb. 2022 27 Feb. 2022
Final versions for preproceedings: was 28 Feb. 2022 14 March 2022
Final versions for EPTCS proceedings: 16 May 2022

14th international Workshop on Rewriting Logic and Its Applications, WRLA 2022

Date: Sat-Sun, April 2-3

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 topics of the workshop include, but are not limited to, foundations and models of rewriting and rewriting logic, uses of rewriting and rewriting logic as a logical and semantic framework, rewriting languages, verification techniques for rewrite theories, and applications of rewriting in various domains, including logic, mathematics, security, software engineering, distributed computing, real-time and cyber-physical systems, physics, biology, etc.

Organizer Kyungmin Bae (POSTECH, South Korea)

Abstracts: was 21 Dec. 2021 4 Jan. 2022
Regular, tool and work-in-progress papers max 15 pp + refs llncs.cls: was 28 Dec. 2021 11 Jan. 2022
Notification: 8 Feb. 2022