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

Wednesday April 6th

Wednesday, April 6th


Invited speaker: Alexandra Silva

The Frontiers of Active Learning in Network Verification

Room: HS1,  online: link, Chair: Jan Křetínský


Coffee break


Constraint Solving

Room: HS1, online: link
Chair: Andreia Mordido

  • Randal Bryant, Armin Biere and Marijn Heule. Clausal Proofs for Pseudo-Boolean Reasoning
  • Joseph Reeves, Marijn Heule and Randal Bryant. Moving Definition Variables in Quantified Boolean Formulas
  • Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K Murali and Christoph Weidenbach. A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
  • Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Noetzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver [nominated for SCP best tool paper]

Monitoring and Analysis
Room: HS2, online: link
Chair: Ezio Bartocci

  • Pu Yi, Hao Wang, Tao Xie, Darko Marinov and Wing Lam. A Theoretical Analysis of Random Regression Test Prioritization
  • Sheila Zingg, Srdjan Krstic, Martin Raszyk, Joshua Schneider and Dmitriy Traytel. Verified First-Order Monitoring with Recursive Rules
  • Ilia Zlatkin and Grigory Fedyukovich. Maximizing Branch Coverage with Constrained Horn Clauses
  • Marco Bozzano, Alessandro Cimatti, Alberto Griggio and Martin Jonáš. Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation

Categorical Models

Room: Interims HS1, online: link
Chair: Jurriaan Rot

  • Anne Broadbent and Martti Karvonen. Categorical composable cryptography
  • Davide Castelnovo, Fabio Gadducci and Marino Miculan. A new criterion for M,N-adhesivity, with an application to hierarchical graphs
  • Dylan McDermott, Exequiel Rivas and Tarmo Uustalu. Sweedler Theory of Monads
  • Guillaume Boisseau and Robin Piedeleu. Graphical Piecewise-Linear Algebra

Verified Systems

Room: HS3, online: link
Chair: Peter Müller

  • Jorge Sousa Pinto, Cláudio Belo Lourenço. Why3-do: The Way of Harmonious Distributed System Proofs [nominated for SCP best tool paper]
  • Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell. Relaxed virtual memory in Armv8-A [nominated for EASST best paper]
  • Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell. Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
  • David Monniaux, Sylvain Boulmé. The Trusted Computing Base of the CompCert Verified Compiler




General Assembly
Room: HS1,  online: link


TACAS: Model checking and verification
Room: HS1, online: link
Chair: Alexandra Silva

  • Nicolas Amat, Silvano Dal Zilio and Thomas Hujsa. Property Directed Reachability for Generalized Petri Nets
  • Martin Blicha, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina. Transition Power Abstractions for Deep Counterexample Detection
  • Marco Bozzano, Alessandro Cimatti, Stefano Tonetta and Viktória Vozárová. Searching for Ribbon-Shaped Paths in Fair Transition Systems
  • Dirk Beyer and Sudeep Kanav. CoVeriTeam: On-Demand Composition of Cooperative Verification Systems

Room: Interims HS1, online: link
Chair: Robert Atkey

  • Simon Gay, Diogo Poças and Vasco Vasconcelos. The Different Shades of Infinite Session Types
  • Emmanuel Hainry, Bruce Kapron, Jean-Yves Marion and Romain Péchoux. Complete and tractable machine-independent characterizations of second-order polytime [nominated for EAPLS and EATCS best paper]
  • José Espírito Santo, Delia Kesner and Loïc Peyrot. A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications
  • André Hirschowitz, Tom Hirschowitz, Ambroise Lafont and Marco Maggesi. Variable binding and substitution for (nameless) dummies

Concurrency I
Room: HS3, online: link
Chair: Rupak Majumdar

  • Eleni Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson. View-Based Owicki–Gries Reasoning for Persistent x86-TSO
  • Artem Khyzha, Ori Lahav. Abstraction for Crash-Resilient Objects
  • Varsha P Suresh, Deepak D'Souza, Rekha Pai, Meenakshi D'Souza, Sujit Kumar Chakrabarti. Static Race Detection for Periodic Programs
  • Parosh Aziz Abdulla and Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait Godbole, Krishna S. Probabilistic Total Store Ordering


Coffee break


ETAPS 25: Celebration of the 25th edition of ETAPS
Room: HS1, online: link (passcode 641339, public), Chair: Marieke Huisman


Banquet at 19:15
Taking place at Nockherberg, a typical beer garden and event location famous for their strong beer festival and the political derbleckn.


Directions to reach the Banquet from university campus:

  • Take U6 from Garching-Forschungszentrum (University campus) U-bahn station.
  • ˆGet off at Sendlinger Tor (15 stops, 27 minutes).
  • Take U2 from Sendlinger Tor towards Messestadt Ost.
  • Get off at Kolumbusplatz (2 stops, 3 minutes).
  • Walk 10 minutes on Nockherstrasse to reach Nockherberg.