TACAS 2021 programme

Game Theory/Model checking (Chair: Marcin Jurdzinski)

• Benjamin Bisping, Uwe Nestmann. A Game for Linear-time–Branching-time Spectroscopy [doi]
• Suguman Bansal, Krishnendu Chatterjee, Moshe Y. Vardi. On Satisficing in Quantitative Games [doi]
• Daniel Hausmann, Lutz Schröder. Quasipolynomial Computation of Nested Fixpoints [doi]
• Tzu-Han Hsu, César Sánchez, Borzoo Bonakdarpour. Bounded Model Checking for Hyperproperties [doi]

TACAS
SMT Verification (Chair: Joost-Pieter Katoen)

• Seulkee Baek, Mario Carneiro, Marijn J. H. Heule. A Flexible Proof Format for SAT Solver-Elaborator Communication [doi]
• Randal E. Bryant, Marijn J. H. Heule. Generating Extended Resolution Proofs with a BDD-Based SAT Solver [doi] (nominated for EATCS best paper award)
• Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays [doi]
• Muhammad Osama, Anton Wijs, Armin Biere. SAT Solving with GPU Accelerated Inprocessing [doi]

17h00 -

18:20 

TACAS 
Probabilities (Chair: David N. Jansen)

• Jip Spel, Sebastian Junges, Joost-Pieter Katoen. Finding Provably Optimal Markov Chains [doi]
• Roman Andriushchenko, Milan Češka, Sebastian Junges, Joost-Pieter Katoen. Inductive Synthesis for Probabilistic Programs Reaches New Horizons [doi]
• Michael Backenköhler, Luca Bortolussi, Gerrit Großmann, Verena Wolf. Analysis of  Markov Jump Processes under Terminal Constraints [doi]
• Tim Quatmann, Joost-Pieter Katoen. Multi-objective Optimization of Long-run Average and Total Rewards [doi]

Timed systems (Chair: Susanne Graf)

• Jaroslav Bendík, Ahmet Sencan, Ebru Aydin Gol, Ivana Černá. Timed Automata Relaxation for Reachability [doi]
• Étienne André, Jaime Arias, Laure Petrucci, Jaco van de Pol. Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata [doi]
• Konstantinos Mamouras, Agnishom Chattopadhyay, Zhifu Wang. Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring [doi]
• Fabian Meyer, Marcel Hark, Jürgen Giesl. Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes [doi]

TACAS 
Neural networks (Chair: Armin Biere)

• Daniel M. Yellin, Gail Weiss. Synthesizing Context-free Grammars from Recurrent Neural Networks [doi]
• Andrea Peruffo, Daniele Ahmed, Alessandro Abate. Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [doi]
• Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, Lijun Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement [doi]
• Guy Amir, Haoze Wu, Clark Barrett, Guy Katz. An SMT-Based Approach for Verifying Binarized Neural Networks [doi]

17h00 -

18h20

TACAS 
Analysis of network communication (Chair: Hossein Hojjat)

• Stefan Schmid, Nicolas Schnepf, Jiří Srba. Resilient Capacity-Aware Routing [doi]
• Lei Shi, Yahui Li, Boon Thau Loo, Rajeev Alur. Network Traffic Classification by Program Synthesis [doi]
• Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche. General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond [doi] (EAPLS best paper award winner)
• Anjiang Wei, Pu Yi, Tao Xie, Darko Marinov, Wing Lam. Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests [doi]

TACAS

Verification techniques (not SMT) (Chair: Jan Strejcek)

• Michael Blondin, Christoph Haase, Philip Offtermatt. Directed Reachability for Infinite-State Systems [doi]
• Grigory Fedyukovich, Gidon Ernst. Bridging Arrays and ADTs in Recursive Proofs [doi]
• Margarida Ferreira, Miguel Terra-Neves, Miguel Ventura, Inês Lynce, Ruben Martins. FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions [doi]
• Nikola Beneš, Luboš Brim, Samuel Pastva, David Šafránek. Symbolic Coloured SCC Decomposition [doi]

TACAS
Case studies/floating point (Chair: Thierry Lecomte)

• Aviad Cohen, Alexander Nadel, Vadim Ryvchin. Local Search with a SAT Oracle for Combinatorial Optimization [doi]
• Julien Lepiller, Ruzica Piskac, Martin Schäf, Mark Santolucito. Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities [doi]
• Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt. Deductive Verification of Floating-Point Java Programs in KeY [doi] (nominated for EAPLS best paper award)
• Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis. A Two-Phase Approach for Conditional Floating-Point Verification [doi]

SV-Comp

Software Verification: 10th Comparative Evaluation (SV-COMP 2021) [doi]

• Dirk Beyer. SV-COMP 2021 Report [doi]
• Vadim Mutilin. CPA-BAM-BnB
• Stephan Holzner. CPAchecker [doi]
• Pavel Andrianov. CPALockator [doi]
• Hernan Ponce de Leon. Dartagnan [doi]
• Martin Spießl. Frama-C
• Zsófia Ádám. Gazer-Theta [doi]
• Simmo Saan. Goblint [doi]
• Malte Mues. JDart [doi]
• Soha Hussein. Java-Ranger
• Ali Shamakhi. JayHorn [doi]
• Gidon Ernst. Korn
• Martin Spießl. MetaVal [doi]
• Marek Chalupa. Symbiotic [doi]
• Matthias Heizmann. Ultimate Automizer

15h40 -

17h00

TACAS 
Tools (verification) (Chair: Thomas Neele)

• Daniela Kaufmann, Armin Biere. AMulet 2.0 for Verifying Multiplier Circuits of Rewriting [doi]
• Manuel Gieseking, Jesko Hecking-Harbusch, Ann Yanich. A Web Interface for Petri Nets with Transits and Petri Games [doi]
• Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi. Helmholtz: A Verifier for Tezos Smart [doi]
• Maximilian A. Köhl, Michaela Klauck, Holger Hermanns. Momba: JANI Meets Python [doi]

15h40 -

17h00

SV-Comp

Open Community Meeting on Software Verification

TACAS
Machine learning/SMT (Chair: Radu Mateescu)

• Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen. cake_lpr: Verified Propagation Redundancy Checking in CakeML [doi]
• Pranav Ashok, Mathias Jackermeier, Jan Křetínský, Christoph Weinhuber, Maximilian Weininger, Mayank Yadav. dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts [doi]
• Matthew Sotoudeh, Aditya V. Thakur. SyReNN: A Tool for Analyzing Deep Neural Networks [doi]
• Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh. MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers [doi]

TACAS
Proof generation/validation (Chair: Laura Kovács)

• Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhaue. Certifying Proofs in the First-Order Theory [doi]
• Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. Syntax-Guided Quantifier Instantiation [doi] (nominated for EATCS best paper award)
• Giles Reger, Johannes Schoisswohl, Andrei Voronkov. Making Theory Reasoning Simpler [doi]
• Yong Kiam Tan, André Platzer. Deductive Stability Proofs for Ordinary Differential Equations [doi]

17h00 -

18h00

TACAS 
Tools (testing and monitoring) (Chair: Frédéric Lang)

• Felipe Gorostiaga, César Sánchez. HLola: a Very Functional Tool for Extensible Stream Runtime Verification [doi]
• Carlos E. Budde, Arnd Hartmanns. Replicating Restart with Prolonged Retrials: An Experimental Report [doi]
• Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian A. Köhl, Yannik Schnitzer, Maximilian Schwenger. RTLola on Board: Testing Real Driving Emissions on Your Phone [doi] (nominated for EASST best paper award)