ETAPS 2021: 27 March-1 April 2021, Luxembourg, Luxembourg (online)

TACAS 2020 programme

All times are in CEST (GMT+2)

Monday, March 29
09h00 - 10h20 TACAS

Bisimulation (Chair: Tom van Dijk)

  • David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren and Anton Wijs. An O(m log n) algorithm for branching bisimilarity on labelled transition systems [doi]
  • Frédéric Lang, Radu Mateescu and Franco Mazzanti. Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities [doi]
  • Xudong Qin and Yuxin Deng.  Verifying Quantum Communication Protocols with Ground Bisimulation [doi]
  • Bernardo Almeida, Andreia Mordido and Vasco T. Vasconcelos. Deciding the bisimilarity of context-free session types [doi]
Tuesday, March 30
09h00 - 10h20 TACAS

Timed & Probabilistic Systems (Chair: David N. Jansen)

  • Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan and Miaomiao Zhang.  Learning One-Clock Timed Automata [doi]
  • Simon Wimmer and Joshua von Mutius. Verified Certification of Reachability Checking for Timed Automata [doi]
  • Ezio Bartocci, Laura Kovács, Miroslav Stankovič. MORA - Automatic Generation of Moment-Based Invariants [doi]
  • Carlos E. Budde, Marco Biagi, Raúl E. Monti, Pedro R. D'Argenio and Mariëlle Stoelinga.  Rare event simulation for non-Markovian repairable fault trees [doi] | Carlos E. Budde FIG: the Finite Improbability Generator [doi]
Wednesday, March 31
09h00 - 10h20

TACAS (parallel session)

Program Verification | Timed Systems (Chair: Richard Bornat)

  • Supratik Chakraborty, Ashutosh Gupta and Divyesh Unadkat.  Verifying Array Manipulating Programs with Full-Program Induction [doi]
  • Dirk Beyer and Matthias Dangl.  Software Verification with PDR: An Implementation of the State of the Art (10 min) [doi]
  • Dirk Beyer, Philipp Wendler: CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering (10 min) [doi]
  • Jan Švejda, Philipp Berger and Joost-Pieter Katoen.  Interpretation-Based Violation Witness Validation for C: NITWIT [doi]
  • Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly and Stefano Tonetta. Safe Decomposition of Startup Requirements: Verification and Synthesis [doi]
09h00 - 10h20

TACAS (parallel session)
Verifying Concurrent Systems (Chair: Dana Fisman)

  • Hadar Frenkel, Orna Grumberg, Corina Pasareanu and Sarai Sheinvald.  Assume, Guarantee or Repair [doi]
  • Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis and Christoph Welzel. Structural Invariants for the Verification of Systems with Parameterized Architectures [doi]
  • Wytse Oortwijn, Marieke Huisman, Sebastiaan Joosten and Jaco van de Pol.  Automated Verification of Parallel Nested DFS [doi]
  • Ruben Hamers and Sung-Shik Jongmans. Discourje: Runtime Verification of Communication Protocols in Clojure [doi]

15h40 -


Probabilistic Systems (Chair: David Parker)

  • Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen and Ufuk Topcu. Scenario-Based Verification of Uncertain MDPs [doi]
  • Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann and Mickael Randour.  Simple Strategies in Multi-Objective MDPs [doi]
  • Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak. Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning [doi]
  • Florian Funke, Simon Jantsch and Christel Baier. Farkas certificates and minimal witnesses for probabilistic reachability constraints [doi]
Thursday, April 1
09h00 - 10h00

TACAS (parallel session)
Games & Automata (Chair: Frédéric Lang) 

  • Thomas Neele, Tim Willemse and Wieger Wesselink.  Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems [doi]
  • Massimo Benerecetti, Daniele Dell'Erba and Fabio Mogavero.  Solving Mean-Payoff Games via Quasi Dominions [doi] (nominated for EATCS best paper award)
  • Dana Angluin, Dana Fisman and Yaara Shoval. Polynomial Identification of $\omega$-Automata [doi]
09h00 - 10h20

TACAS (parallel session)
Tools & case studies | Efficiency (Chair: Dirk Beyer)

  • Hans-Dieter Hiep, Olaf Maathuis, Jinting Bian, Frank de Boer, Marko Van Eekelen and Stijn de Gouw. Verifying OpenJDK’s LinkedList using KeY [doi]
  • Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu and Ralf Treinen. Analysing installation scenarios of Debian packages [doi]
  • Richard Bornat, Jaap Boender, Florian Kammueller, Guillaume Poly and Rajagopal Nagarajan. Describing and Simulating Concurrent Quantum Systems [doi]
  • Mirco Giacobbe, Thomas Henzinger and Mathias Lechner.  How Many Bits Does It Take to Quantize Your Neural Network? [doi]
10h40 - 12h00

Logic and Proof | Dynamical Systems (Chair: David Parker)

  • Karl Palmskog, Ahmet Celik and Milos Gligoric. Practical Machine-Checked Formalization of Change Impact Analysis [doi]
  • Umang Mathur, P. Madhusudan and Mahesh Viswanathan.  What's Decidable About Program Verification Modulo Axioms? [doi]
  • Alexander Lochmann and Aart Middeldorp.  Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting [doi]
  • Juraj Kolčák, Jérémy Dubut, Ichiro Hasuo, Shin-Ya Katsumata, David Sprunger and Akihisa Yamada.  Relational Differential Dynamic Logic [doi]

15h20 - 16h40

Model Checking and Reachability | Timed & Dynamical Systems (Chair: Tom van Dijk)

  • S. Akshay, Paul Gastin, Krishna S and Sparsa Roychoudhary. Revisiting Underapproximate Reachability for Multipushdown Systems [doi]
  • Alex Dixon and Ranko Lazic. KReach: A Tool for Reachability in Petri Nets [doi]
  • Hussein Sibai, Navid Mokhlesi, Chuchu Fan and Sayan Mitra. Multi-Agent Safety Verification using Symmetry Transformations [doi]
  • Makai Mann and Clark Barrett. Partial Order Reduction for Deep Bug Finding in Synchronous Hardware [doi]