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

Thursday April 7th

Thursday, April 7th

09:00-
10:00

Invited speaker: Lenore Zuck

RFCs vs Specifications

Room: HS1 Chair: Dana Fisman

10:00-
10:30

Coffee break

10:30-
12:30

TACAS: Probabilistic / Stochastic Systems
Room: HS1, online: link
Chair: Lenore Zuck

  • Ji Guan and Nengkun Yu. A Probabilistic Logic for Verifying Continuous-time Markov Chains
  • Alexander Bork, Joost-Pieter Katoen and Tim Quatmann. Under-Approximating Expected Total Rewards in POMDPs
  • Arnd Hartmanns. Correct Probabilistic Model Checking with Floating-Point Arithmetic
  • Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos. Correlated Equilibria and Fairness in Concurrent Stochastic Games

TACAS: Tools - Optimizations, Repair and Explainability
Room: HS2, online: link
Chair: Marie-Christine Jakobs

  • Steffan Sølvsten, Jaco van de Pol, Anna Blume Jakobsen and Mathias Weller Berg Thomasen. Adiar: Binary Decision Diagrams in External Memory
  • Alnis Murtovi, Alexander Bainczyk and Bernhard Steffen. Forest GUMP: A Tool for Explanation
  • Ömer Şakar, Mohsen Safari, Marieke Huisman and Anton Wijs. Alpinist: an Annotation-Aware GPU Program Optimizer
  • Lei Shi, Yuepeng Wang, Boon Thau Loo and Rajeev Alur. Automatic Repair for Network Programs

ESOP: Type Theory

Room: HS3, online: link
Chair: Max S. New

  • Daniel Marshall, Michael Vollmer, and Dominic Orchard. Linearity and Uniqueness: An Entente Cordiale
  • James Wood and Robert Atkey. A Framework for Substructural Type Systems
  • Pritam Choudhury, Harley Eades, Stephanie Weirich. A Dependent Dependency Calculus
  • Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning. Polarized Subtyping

12:30-
14:00

Lunch

14:00-
16:00

TACAS: ω-automata
Room: HS1, online: link
Chair: Jan Křetínský

  • Tamajit Banerjee, Majumdar Rupak, Mallik Kaushik, Anne-Kathrin Schmuck and Sadegh Soudjani. A Direct Symbolic Algorithm for Solving Stochastic Rabin Games [nominated for EATCS best paper]
  • Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin and Salomon Sickert. Practical Applications of the Alternating Cycle Decomposition
  • Vojtěch Havlena, Ondrej Lengal and Barbora Šmahlíková. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation
  • Maurice Laveaux, Wieger Wesselink and Tim Willemse. On-The-Fly Solving for Symbolic Parity Games

TACAS: SV-COMP 1
Room: HS2, online: link
Chair: Dirk Beyer

  • Intro and Report (Dirk Beyer)
  • AProVE (Jera Hensel)
  • CSeq (Emerson Sales)
  • Dartagnan (Hernan Ponce de Leon)
  • Frama-C-SV (Martin Spiessl)
  • GDart / JDart (Malte Mues)
  • GWit (Falk Howar)
  • LART (Henrich Lauko)
  • Korn (Gidon Ernst)
  • Symbiotic 9 (Marek Chalupa)
  • Symbiotic-Witch (Paulína Ayaziová)
  • Theta (Zsófia Ádám)
  • Ultimate GemCutter (Dominik Klumpp)
  • VeriAbs  (Priyanka Darke)
  • Wit4Java (Tong Wu)

ESOP: Control and Effects
Room: HS3, online: link
Chair: Dominic Orchard

  • Winner of the ETAPS doctoral dissertation award
  • Zhixuan Yang, Marco Paviotti, Nicolas Wu, Birthe van den Berg, Tom Schrijvers. Structured Handling of Scoped Effects
  • Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann. Region-based Resource Management and Lexical Exception Handlers in Continuation-Passing Style

16:00-
16:30

Coffee break

16:30-
18:00

TACAS: Equivalence Checking
Room: HS1, online: link
Chair: Alessandro Cimatti

  • Fabian Birkmann, Hans-Peter Deifel and Stefan Milius. Distributed Coalgebraic Partition Refinement
  • Vasileios Koutavas, Yu-Yang Lin and Nikos Tzevelekos. From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
  • Simon Guilloud and Viktor Kunčak. Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

TACAS: SV-COMP 2
Room: HS2, online: link
Chair: Dirk Beyer

  • Infer-SV (Matthias Kettl)
  • Community Meeting

ESOP: Concurrency II
Room: HS3, online: link
Chair: Robert Atkey

  • Sung-Shik Jongmans, Petra van den Bos. A Predicate Transformer for Choreographies [nominated for EAPLS and EATCS best paper]
  • Rob van Glabbeek. Comparing the expressiveness of the π-calculus and CCS
  • Jana Wagemaker, Nate Foster, Tobias Kappé, Dexter Kozen, Jurriaan Rot, Alexandra Silva. Concurrent NetKAT