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

Monday April 4th


Monday, April 4th


Registration opens


ETAPS opening
Room: HS1, online: link


Invited speaker: Tomas Vojnar

Counting Automata for Efficient Regex Matching and ReDoS Generation

Room: HS1 Chair: Marieke Huisman


Coffee break


TACAS: Synthesis
Room: HS1, online: link
Chair: Rupak Majumdar

  • Gourav Takhar, Ramesh Karri, Christian Pilato and Subhajit Roy. HOLL: Program Synthesis for Higher Order Logic Locking
  • Orna Kupferman and Noam Shenwald. The Complexity of LTL Rational Synthesis
  • Kedar Namjoshi and Nisarg Patel. Synthesis of Compact Strategies for Coordination Programs
  • Yi Lin, Lucas M. Tabajara and Moshe Y. Vardi.  ZDD Boolean Synthesis

FASE: Verification Technology
Room: HS2, online: link
Chair: Heike Wehrheim

  • Dirk Beyer, Sudeep Kanav and Cedric Richter. Construction of Verifier Combinations Based on Off-the-Shelf Verifiers
  • Liqian Chen, Renjie Huang, Dan Luo, Chenghu Ma, Dengping Wei and Ji Wang. Estimating Worst-case Resource Usage by Resource-usage-aware Fuzzing
  • Zunchen Huang and Chao Wang. Symbolic Predictive Cache Analysis for Out-of-Order Execution
  • Marie-Christine Jakobs and Maik Wiesner. PEQtest: Testing Functional Equivalence

FoSSaCS: Program and System Analysis
Room: Interims HS1, online: link
Chair: Nathalie Bertrand

  • Michael Blondin and Javier Esparza. Separators in Continuous Petri Nets
  • A. R. Balasubramanian, Lucie Guillou and Chana Weil-Kennedy. Parameterized Analysis of Reconfigurable Broadcast Networks
  • Georgiana Caltais, Hossein Hojjat, Mohammadreza Mousavi and Hünkar Can Tunç. DyNetKAT: An Algebra of Dynamic Networks [nominated for EASST best paper]
  • Flavio Ascari, Roberto Bruni and Roberta Gori. Limits and difficulties in the design of under-approximation abstract domains




TACAS: Verification
Room: HS1, online: link
Chair: Javier Esparza

  • André Greiner-Petter, Howard Cohl, Abdou Youssef, Moritz Schubotz, Avi Trost, Rajen Dey, Akiko Aizawa and Bela Gipp. Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems
  • Wenhao Wu, Jan Hueckelheim, Paul Hovland and Stephen Siegel. Verifying Fortran Programs with CIVL
  • Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella and Marco Zamboni. NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
  • Haoze Wu, Aleksandar Zeljić, Guy Katz and Clark Barrett. Efficient Neural Network Analysis with Sum-of-Infeasibilities

FASE: AI & Quantitative Methods
Room: HS2, online: link
Chair: Andrzej Wasowski

  • Evangelos Papathomas, Themistoklis Diamantopoulos and Andreas Symeonidis. Semantic Code Search in Software Repos using Neural Machine Translation
  • Sai Sathiesh Rajan, Sakshi Udeshi and Sudipta Chattopadhyay. AequeVox: Automated Fairness Testing of Speech Recognition Systems
  • Saikat Dutta, Zixin Huang and Sasa Misailovic. SixthSense: Debugging Convergence Problems in Probabilistic Programs via Program Representation Learning
  • Aleksandar S. Dimovski. Quantitative Program Sketching using Lifted Static Analysis

FoSSaCS: Temporal Logic and Processes
Room: Interims HS1, online: link
Chair: Stefan Milius

  • Tobias Winkler, Christina Gehnen and Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs
  • Christel Baier, Florian Funke, Jakob Piribauer and Robin Ziemek. On probability-raising causality in Markov decision processes [nominated for EATCS best paper]
  • Bernd Finkbeiner, Philippe Heim and Noemi Passing. Temporal Stream Logic modulo Theories

FASE: Test-Comp 1

Room: HS3, online: link
Chair: Dirk Beyer

  • Report.
    Dirk Beyer
  • CoVeriTest.
    Marie-Christine Jakobs
  • FuSeBMC. Kaled Alshmrany
  • Legion/SymCC.
    Gidon Ernst
  • TestCov.
    Thomas Lemberger
  • VeriFuzz.
    Ravindra Metta


Coffee break


TACAS: Blockchain
Room: HS1, online: link
Chair: Georgiana Caltais

  • Franck Cassez, Joanne Fuller and Aditya Asgaonkar. Formal Verification of the Ethereum 2.0 Beacon Chain
  • David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu and Emma Zhong. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover [nominated for  EAPLS best paper and SCP best tool paper]
  • Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo and Albert Rubio. A Max-SMT Superoptimizer for EVM handling Memory and Storage

Invited tutorial: Stacey Jeffery

Quantum Algorithms

Room: Interims HS1, online: link
Chair: Lenore Zuck


FASE: Test-Comp 2

Room: HS3, online: link
Chair: Dirk Beyer

  • Community Meeting


Reception at 19:00 (last drink at 22:30)
Taking place at the cafe Reitschule.



Directions to reach the Reception from university campus:

  • Take U6 from Garching-Forschungszentrum (University campus) U-bahn station.
  • Get off at Giselastraße (11 stops, 21 minutes).
  • Walk 5 minutes on Giselastraße to reach Café Reitschule.