TACAS 2021 Accepted Papers

Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue and Lijun Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement

Jaroslav Bendík, Ahmet Sencan, Ebru Aydin Gol and Ivana Černá. Timed Automata Relaxation for Reachability

Randal E. Bryant and Marijn J. H. Heule. Generating Extended Resolution Proofs with a BDD-Based SAT Solver

Michael Blondin, Christoph Haase and Philip Offtermatt. Directed Reachability for Infinite-State Systems

Guy Amir, Haoze Wu, Clark Barrett and Guy Katz. An SMT-Based Approach for Verifying Binarized Neural Networks

Yong Kiam Tan, Marijn Heule and Magnus O. Myreen. cake_lpr: Verified Propagation Redundancy Checking in CakeML

Tzu-Han Hsu, Cesar Sanchez and Borzoo Bonakdarpour. Bounded Model Checking for Hyperproperties

Felipe Gorostiaga and Cesar Sanchez. HLola: a Very Functional Tool for Extensible Stream Runtime Verification

Fabian Meyer, Marcel Hark and Jürgen Giesl. Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes

Étienne André, Jaime Arias, Laure Petrucci and Jaco van de Pol. Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata

Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon and Clark Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

Daniela Kaufmann and Armin Biere. AMulet 2.0 for Verifying Multiplier Circuits

Aviad Cohen, Alexander Nadel and Vadim Ryvchin. Local Search with a SAT Oracle for Combinatorial Optimization

Michael Backenköhler, Luca Bortolussi, Gerrit Großmann and Verena Wolf. Analysis of Markov Jump Processes under Terminal Constraints

Benjamin Bisping and Uwe Nestmann. A Game for Linear-time–Branching-time Spectroscopy

Yong Kiam Tan and André Platzer. Deductive Stability Proofs for Ordinary Differential Equations

Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova and Maria Christakis. A Two-Phase Approach for Conditional Floating-Point Verification

Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich and Wolfgang Ahrendt. Deductive Verification of Floating-Point Java Programs in KeY

Yuki Nishida, Hiromasa Saito, Chen Ran, Akira Kawata, Jun Furuse, Kouhei Suenaga and Atsushi Igarashi. Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types

Stefan Schmid, Nicolas Schnepf and Jiri Srba. Resilient Capacity-Aware Routing

Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian Köhl, Yannik Schnitzer and Maximilian Schwenger. RTLola on Board: Testing Real Driving Emissions on your Phone

Margarida Ferreira, Miguel Terra-Neves, Miguel Ventura, Inês Lynce and Ruben Martins. FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions

Carlos E. Budde and Arnd Hartmanns. Replicating Restart with Prolonged Retrials: An Experimental Report

Andrea Peruffo, Daniele Ahmed and Alessandro Abate. Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models

Giles Reger, Johannes Schoisswohl and Andrei Voronkov. Making Theory Reasoning Simpler

Nikola Benes, Lubos Brim, Samuel Pastva and David Šafránek. Symbolic Coloured SCC Decomposition

Seulkee Baek, Mario Carneiro and Marijn Heule. A Flexible Proof Format for SAT Solver-Elaborator Communication

Matthew Sotoudeh and Aditya Thakur. SyReNN: A Tool for Analyzing Deep Neural Networks

Suguman Bansal, Krishnendu Chatterjee and Moshe Vardi. On Satisficing in Quantitative Games

Roman Andriushchenko, Milan Ceska, Sebastian Junges and Joost-Pieter Katoen. Inductive Synthesis for Probabilistic Programs Reaches New Horizons

Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati and Vijay Ganesh. MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers

Konstantinos Mamouras, Agnishom Chattopadhyay and Zhifu Wang. Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring

Tim Quatmann and Joost-Pieter Katoen. Multi-objective Optimization of Long-run Average and Total Rewards

Grigory Fedyukovich and Gidon Ernst. Bridging Arrays and ADTs in Recursive Proofs

Julien Lepiller, Ruzica Piskac, Martin Schaef and Mark Santolucito. Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. Syntax-Guided Quantifier Instantiation

Lei Shi, Yahui Li, Boon Thau Loo and Rajeev Alur. Network Traffic Classification by Program Synthesis

Anjiang Wei, Pu Yi, Tao Xie, Darko Marinov and Wing Lam. Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests

Daniel Yellin and Gail Weiss. Synthesizing Context-free Grammars from Recurrent Neural Networks

Manuel Gieseking, Jesko Hecking-Harbusch and Ann Yanich. A Web Interface for Petri Nets with Transits and Petri Games

Muhammad Osama, Anton Wijs and Armin Biere. SAT Solving with GPU Accelerated Inprocessing

Rupak Majumdar, Ramanathan Thinniyam Srinivasan and Georg Zetzsche. General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond

Alexander Lochmann, Fabian Mitterwallner, Aart Middeldorp and Bertram Felgenhauer. Certifying Proofs in the First-Order Theory of Rewriting

Jip Spel, Sebastian Junges and Joost-Pieter Katoen. Finding Provably Optimal Markov Chains

Maximilian Alexander Köhl, Michaela Klauck and Holger Hermanns. Momba: JANI Meets Python

Pranav Ashok, Mathias Jackermeier, Jan Kretinsky, Christoph Weinhuber, Maximilian Weininger and Mayank Yadav. dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts

Daniel Hausmann and Lutz Schröder. Quasipolynomial Computation of Nested Fixpoints