ETAPS 2022: 2-7 April 2022, Munich, Germany

Tuesday April 5th

Tuesday, April 5th


Invited speaker: Nathalie Bertrand

Parameterized verification to the rescue of distributed algorithms

Room: HS1, online: link Chair: Lutz Schröder


Coffee break


TACAS: Grammatical Inference

Room: HS1, online: link
Chair: Delia Kesner

  • Frits Vaandrager, Bharat Garhewal, Jurriaan Rot and Thorsten Wissmann. A New Approach for Active Automata Learning Based on Apartness
  • Véronique Bruyère, Guillermo Pérez and Gaëtan Staquet. Learning Realtime One-Counter Automata
  • Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow and Daniel Neider. Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic
  • Luca Bortolussi, Giuseppe Maria Gallo, Jan Kretinsky and Laura Nenzi. Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes [nominated for EASST best paper]

FASE: Trustworthiness & Adaptability

Room: HS2, online: link
Chair: Marie-Christine Jakobs

  • Ezio Bartocci, Thomas Ferrère, Thomas Henzinger, Dejan Nickovic and Ana Oliveira Da Costa. Information-flow Interfaces [nominated for EASST best paper]
  • Lukas Grätz, Reiner Hähnle and Richard Bubel. Finding Semantic Bugs Fast
  • Sebastian Biewer and Holger Hermanns. On the Detection of Doped Software by Falsification
  • Simon Robillard and Helene Coullon. SMT-Based Planning Synthesis for Distributed System Reconfigurations

FoSSaCS: Automata, Games and Regular Languages
Room: Interims HS1, online: link
Chair: Javier Esparza

  • Udi Boker and Karoliina Lehtinen. Token Games and History-Deterministic Quantitative-Automata
  • Dana Angluin, Timos Antonopoulos, Dana Fisman and Nevin George. Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata
  • Thomas Colcombet, Sam van Gool and Rémi Morvan. First-order separation over countable ordinals
  • Udi Boker, Karoliina Lehtinen and Salomon Sickert. On the Translation of Automata to Linear Temporal Logic




TACAS: Verification Inference
Room: HS1, online: link
Chair: Simon Robillard

  • Jonas Krämer, Lionel Blatter, Eva Darulova and Mattias Ulbrich. Inferring Interval-Valued Floating-Point Preconditions
  • Dawei Sun and Sayan Mitra. NeuReach: Learning Reachability Functions from Simulations
  • Jason Koenig, Oded Padon, Sharon Shoham and Alex Aiken. Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
  • Brandon Paulsen and Chao Wang. LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions

FASE: Model-Based Engineering
Room: HS2, online: link
Chair: Marielle Stoelinga

  • Alexander Knapp, Markus Roggenbach and Tobias Rosenberger. An Institutional Approach to Communicating UML State Machines
  • Edouard Batot, Sebastien Gerard and Jordi Cabot. A Survey-Based Feature Model for Software Traceability
  • Hannes Thaller, Lukas Linsbauer and Alexander Egyed. Semantic Clone Detection via Probabilistic Software Modeling
  • Hao Wu. QMaxUSE: A Query-based Verification Tool for UML Class Diagrams with OCL Invariants (Tool Demo)
  • Hassan Hage, M Seferis, Vahid Hashemi and Frank Mantwill. SMC4PEP: Stochastic Model Checking of Product Engineering Processes (Tool Demo)

FoSSaCS: Logic and Complexity
Room: Interims HS1, online: link
Chair: Patricia Bouyer

  • Raul Fervari and Alessio Mansutti. Modal Logics and Local Quantifiers: A Zoo in the Elementary Hierarchy
  • Reijo Jaakkola. Uniform guarded fragments
  • Dmitry Chistikov, Christoph Haase and Alessio Mansutti. Quantifier elimination for counting extensions of Presburger arithmetic
  • Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari and Stefano Tonetta. A first-order logic characterisation of safety and co-safety languages

ESOP: Semantics and Randomness
Room: HS3, online: link
Chair: Ilya Sergey

  • Geoff Cruttwell, Bruno Gavranovic, Neil Ghani, Paul Wilson, Fabio Zanasi. Categorical Foundation of Gradient-Based Learning [nominated for EATCS best paper]
  • Daniel Lundén, Joey Öhman, Jan Kudlicka, Viktor Senderov, Fredrik Ronquist, David Broman.Compiling Universal Probabilistic Programming Languages with Efficient Parallel Sequential Monte Carlo Inference
  • Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Kessler, Christoph Matheja, Thomas Noll. Foundations for Entailment Checking in Quantitative Separation Logic
  • Hideki Tsuiki, Ulrich Berger. Extracting total Amb programs from proofs


Coffee break


TACAS: Short papers
Room: HS1, online: link
Chair: Alexander Knapp

  • Keigo Imai, Julien Lange and Rumyana Neykova. Kmclib: Automated Inference and Verification of Session Types from OCaml Programs
  • Ivan Perez, Anastasia Mavridou, Tom Pressburger, Alwyn Goodloe and Dimitra Giannakopoulou. Automated Translation of Natural Language Requirements to Runtime Monitors
  • Luciano Putruele, Ramiro Demasi, Pablo Castro and Pedro R. D'Argenio. MaskD: A Tool for Measuring Masking Fault-Tolerance
  • Aleksandar Chakarov, Aleksandr Fedchin, Zvonimir Rakamarić and Neha Rungta. Better Counterexamples for Dafny

Invited tutorial: Nicholas Lane /
Pedro Porto Buarque de Gusmão

Federated Learning with Flower

Room: Interims HS1, online: link
Chair: Dirk Beyer



SC Meeting