# 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

TACAS is a forum for researchers, developers and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, flexibility and efficiency of tools and algorithms for building systems.

Theoretical papers with clear relevance for tool construction and analysis as well as tool descriptions and case studies with a conceptual message are all encouraged. The topics covered by the conference include, but are not limited to:

- specification and verification techniques;
- software and hardware verification;
- analytical techniques for real-time, hybrid, or stochastic systems;
- analytical techniques for safety, security, or dependability;
- SAT and SMT solving;
- theorem proving;
- model checking;
- static and dynamic program analysis;
- testing;
- abstraction techniques for modeling and verification;
- compositional and refinement-based methodologies;
- system construction and transformation techniques;
- machine-learning techniques for synthesis and verification;
- tool environments and tool architectures;
- applications and case studies.

## Important dates, paper submission and review

See the ETAPS 2022 joint call for papers. Submit your paper via the TACAS 2022 author interface of EasyChair.

If you will submit an artifact by 4 November, then register it already by the paper submission deadline of 14 October. Have a line as follows at the end of the paper abstract:

"Data Availability Statement: An artifact will be submitted to the AEC under EasyChair id XYZ."

Have the following as the title of the artifact:

"Artifact for Paper (papertitle)"

The review process of TACAS 2022 is single-blind, with a rebuttal phase for selected papers.

Limit of 4 submissions: Each individual author is limited to a maximum of four TACAS submissions as an author or co-author. Authors of co-authored submissions are jointly responsible for respecting this policy. In case of violations, all submissions of this (co-)author will be desk-rejected.

## Paper categories

TACAS accepts four types of submissions: research papers, case-study papers, regular tool papers, and tool demonstration papers.

Research papers clearly identify and justify a principled advance to the theoretical foundations for the construction and analysis of systems. Where applicable, they are supported by experimental validation.

Case-study papers report on case studies, preferably in a real-world setting. They should provide information about the following aspects: the system being studied and the reasons why it is of interest, the goals of the study, the challenges the system poses to automated analysis/testing/synthesis, research methodologies and approaches used, the degree to which the goals were met, and how the results can be generalized to other problems and domains.

Regular tool papers present a new tool, a new tool component, or novel extensions to an existing tool, and are subject to an artifact submission requirement (see below). They should provide a short description of the theoretical foundations with relevant citations, and emphasize the design and implementation concerns, including software architecture and core data structures. A regular tool paper should give a clear account of the tool’s functionality, discuss the tool’s practical capabilities with reference to the type and size of problems it can handle, describe experience with realistic case studies, and where applicable, provide a rigorous experimental evaluation. Papers that present extensions to existing tools should clearly focus on the improvements or extensions with respect to previously published versions of the tool, preferably substantiated by data on enhancements in terms of resources and capabilities.

Tool-demonstration papers focus on the usage aspects of tools and are also subject to the artifact submission requirement. Theoretical foundations and experimental evaluation are not required, however, a motivation as to why the tool is interesting and significant should be provided. Further, the paper should describe aspects such as, for example, the assumptions about application domain and/or extent of potential generality, demonstrate the tool workflow(s), explain integration and/or human interaction, evaluate the overall role and the impact to the development process.

The length of research, case study, and regular tool papers is limited to 16 pp llncs.cls (excluding the bibliography). The length of tool demonstration papers is limited to 6 pp llncs.cls (excluding the bibliography). Additional material can be placed in a clearly marked appendix. The reviewers are, however, not obliged to read such appendices. If the paper is accepted, a full version including the appendix should be made publicly available via arXiv or a similar platform.

## Paper evaluation

All papers will be evaluated by the program committee (PC), coordinated by the PC chairs, aided by the case study chair for case study papers, and by the tools chair for regular tool papers and tool demonstration papers. All papers will be judged on novelty, significance, correctness, and clarity.

Reproducibility of results is of the utmost importance for the TACAS community. Therefore, we encourage all authors to include support for replicating the results of their papers. For theorems, this would mean providing proofs; for algorithms, this would mean including evidence of correctness and acceptable performance, either by a theoretical analysis or by experimentation; and for experiments, one should provide access to the artifacts used to generate the experimental data. Material that does not fit into the paper may be provided on a supplementary web site, with access appropriately enabled and license rights made clear. For example, the supplemental material for reviewing case-study papers and papers with experimental results could be classified as reviewer-confidential if necessary (e.g., if proprietary data are investigated or software is not open source). In general, TACAS encourages all authors to archive additional material and make it citable via DOI (e.g., via Zenodo or Figshare).

## Artifact submission and evaluation

Regular tool papers and tool demonstration papers must be accompanied by an artifact, registered by the paper submission deadline and submitted by the specific deadline shortly after.

Exceptions to the compulsory artifact submission rule may be granted by the AEC chairs, but only in cases when the tool cannot in any reasonable way be run by the AEC. In such cases, the authors should contact the AEC chairs as soon as possible (at least 7 days prior to abstract submission), ask for an exception, and explain why it is needed. An example of a case where an exception can be negotiated is a tool that must be run in some very special environment, e.g., on special hardware that cannot be virtualised in any way. Note that license problems are generally not an acceptable grounds for an exception. When an exception is granted, the authors should instead submit a detailed video showing their tool in action.

The artifact will be evaluated by the artifact evaluation committee (AEC) independently of the paper according to the following criteria:

consistency with and replicability of results in the paper,
completeness,
documentation, and
ease of use.

The results of the artifact evaluation will be taken into account during discussion of the paper submission.

For research papers and case study papers, pre-paper-acceptance submission of an artifact is optional. If an artifact is provided at this point, then it will be reviewed at this stage by the AEC and the results of the evaluation can be taken into consideration during the paper reviewing and rebuttal phase. Alternatively, authors of papers of these categories may submit an artifact for evaluation after the paper has been accepted.

More information can be found on the TACAS-specific web site.

## Competition on software verification

TACAS 2022 will host the next, 11th instance of the Competition on Software Verification, SV-COMP.

## Invited speaker

Lenore Zuck, University of Illinois at Chicago, USA

## Program chairs

Dana Fisman (Ben-Gurion University of the Negev, Israel)
Grigore Rosu (University of Illinois at Urbana-Champaign, USA)

## Program committee

Parosh Aziz Abdulla (Uppslala University, Sweden)
Luca Aceto (Reykjavik University, Iceland)
Timos Antonopoulos (Yale University, USA)
Saddek Bensalem (Verimag, Université Grenoble Alpes, France)
Dirk Beyer (Ludwig-Maximilians-Universität München, Germany)

Nikolaj Bjørner (Microsoft Research, USA)
Jasmine Blanchette (Vrije Universiteit Amsterdam, The Netherlands)
Udi Boker (Interdisciplinary Center Herzliya, Israel)
Hana Chockler (King's College London, UK)
Rance Cleaveland (University of Maryland, USA)

Alessandro Coglio (Kestrel Institute, USA)
Pedro D'Argenio (Universidad Nacional de Córdoba, CONICET, Argentina)
Javier Esparza (Technische Universität München, Germany)
Bernd Finkbeiner (CISPA Helmholtz Center for Information Security, Germany)
Martin Fränzle (OFFIS GmbH)

Susanne Graf (Verimag, CNRS, France)
Radu Grosu (Technische Universität Wien, Austria / Stony Brook University, USA)
Arie Gurfinkel (University of Waterloo, Canada)
Klaus Havelund (Jet Propulsion Lab, USA)
Holger Hermanns (Universität des Saarlandes, Germany)

Falk Howar (Technische Universität Clausthal / IPSSE, Germany)
Swen Jacobs (CISPA, Germany)
Ranjit Jhala (University of California at San Diego, USA)
Jan Křetínský (Technische Universität München, Germany)
Viktor Kunčak (EPF Lausanne, Switzerland)

Kim G. Larsen (Aalborg University, Denmark)
Konstantinos Mamouras (Rice University, USA)
Daniel Neider (MPI-SWS, Germany)
Dejan Ničković (Austrian Institute of Technology, Austria)
Corina Pasareanu (NASA Ames RC / Carnegie Mellon University, USA)

Doron Peled (Bar Ilan University, Israel)
Anna Philippou (University of Cyprus, Cyprus)
Kristin Yvonne Rozier (Iowa State University, USA)
César Sánchez (IMDEA Software Institute, Spain)
Sven Schewe (University of Liverpool, UK)

Natasha Sharygina (Università della Svizzera italiano, Switzerland)
Jan Strejček (Masaryk University, Czechia)
Cesare Tinelli (University of Iowa, USA)
Stavros Tripakis (Northeastern University, USA)
Frits Vaandrager (Radboud Universiteit Nijmegen, The Netherlands)

Tomáš Vojnar (Brno University of Technology, Czechia)
Christoph M. Wintersteiger (Microsoft, USA)
Lijun Zhang (Institute of Software, Chinese Academy of Sciences, China)
Lingming Zhang (University of Illinois at Urbana-Champaign, USA)
Lenore Zuck (University of Illinois in Chicago, USA)

## Case study and tools chairs

Swen Jacobs (CISPA, Germany)
Andrew Reynolds (University of Iowa, USA)

## Competition chair

Dirk Beyer (Ludwig-Maximilians-Universität München, Germany)

## Competition committee

See competition web site.

## Artifact evaluation chairs

Swen Jacobs (CISPA, Germany)
Andrew Reynolds (University of Iowa, USA)

## Artifact evaluation committee

Pavel Andrianov (Institute of Systems Programming, Russian Academy of Sciences, Russia)
Michael Backenköhler (Universität des Saarlandes Germany)
Sebastian Biewer (Universität des Saarlandes, Germany)
Benjamin Bisping (Technische Universität Berlin, Germany)
Olav Bunte (Technische Universiteit Eindhoven, The Netherlands)
Damien Busatto-Gaston (Université Libre de Bruxelles, Belgium)
Marek Chalupa (Masaryk University, Czechia)
Priyanka Darke (Tata Consultancy Services, India)
Mathias Fleury (Johannes-Kepler-Universität Linz, Austria)
Felipe Gorostiaga (IMDEA Software Institute, Spain)
Kush Grover (Technische Universität München, Germany)
Daniela Kaufmann (Johannes-Kepler-Universität Linz, Austria)
Mitja Kulczynski (Universität zu Kiel, Germany)
Maximilian Alexander Köhl (Universität des Saarlandes, Germany)
Maurice Laveaux (Technische Universiteit Eindhoven, The Netherlands)
Yong Li (Institute of Software, Chinese Academy of Sciences, China)
Debasmita Lohar (Max Planck Institute for Software Systems, Germany)
Makai Mann (Stanford University, USA)
Stefanie Mohr (Technische Universität München, Germany)
Malte Mues (Technische Universität Dortmund, Germany)
Yuki Nishida (Kyoto University, Japan)
Philip Offtermatt (Université de Sherbrooke. Canada)
Muhammad Osama (Technische Universiteit Eindhoven, The Netherlands)
Mathias Preiner (Stanford University, USA)
José Proença (ISEP and INESC TEC, Portugal)
Tim Quatmann (RWTH Aachen, Germany)
Étienne Renault (LRDE, France)
Morten Konggaard Schou (Aalborg University, Denmark)
Michael Schwarz (Technische Universität München, Germany)
Joseph Scott (University of Waterloo, Canada)
Ali Shamakhi (University of Tehran, Iran)
Lei Shi (University of Pennsylvania, USA)
Matthew Sotoudeh (University of California at Davis, USA)
Jip Spel (RWTH Aachen, Germany)
Veronika Šoková (Brno University of Technology, Czechia)

## Steering committee chair

Joost-Pieter Katoen (RWTH Aachen, Germany / Universiteit Twente, The Netherlands)

## Steering committee

Dirk Beyer (Ludwig-Maximilians-Universität München, Germany)
Rance Cleaveland (University of Maryland, USA)
Holger Hermanns (Universität des Saarlandes, Germany)
Kim G. Larsen (Aalborg University, Denmark)
Bernhard Steffen (Technische Universität Dortmund, Germany)