TACAS 2020 programme

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]

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]

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]

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 -

17h00

TACAS 
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]

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]

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]

TACAS
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

TACAS 
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]