TACAS 2020 Accepted Papers
- Frédéric Lang, Radu Mateescu and Franco Mazzanti. Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
- 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
- Hadar Frenkel, Orna Grumberg, Corina Pasareanu and Sarai Sheinvald. Assume, Guarantee or Repair
- Carlos E. Budde. FIG: the Finite Improbability Generator
- Makai Mann and Clark Barrett. Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
- Aman Goel and Karem Sakallah. AVR: Abstractly Verifying Reachability
- Wytse Oortwijn, Marieke Huisman, Sebastiaan Joosten and Jaco van de Pol. Automated Verification of Parallel Nested DFS
- Thomas Neele, Tim Willemse and Wieger Wesselink. Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
- Freek Verbeek, Joshua Bockenek and Binoy Ravindran. Highly Automated Formal Proofs over Memory Usage of Assembly Code
- Jan Svejda, Philipp Berger and Joost-Pieter Katoen. Interpretation-Based Violation Witness Validation for C: NITWIT
- Takamasa Okudono and Andy King. Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
- Florian Funke, Simon Jantsch and Christel Baier. Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Dirk Beyer and Matthias Dangl. Software Verification with PDR: An Implementation of the State of the Art
- Dirk Beyer and Philipp Wendler. CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering
- Alexander Lochmann and Aart Middeldorp. Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
- Daniele Ahmed, Andrea Peruffo and Alessandro Abate. Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
- Jaroslav Bendík and Ivana Cerna. MUST: Minimal Unsatisfiable Subsets Enumeration Tool
- Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly and Stefano Tonetta. Safe Decomposition of Startup Requirements: Verification and Synthesis
- Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu and Ralf Treinen. Analysing installation scenarios of Debian packages
- Massimo Benerecetti, Daniele Dell'Erba and Fabio Mogavero. Solving Mean-Payoff Games via Quasi Dominions
- David Castro-Perez, Francisco Ferreira and Nobuko Yoshida. EMTST: Engineering the Meta-theory of Session Types
- Xudong Qin and Yuxin Deng. Verifying Quantum Communication Protocols with Ground Bisimulation
- Hans-Dieter Hiep, Olaf Maathuis, Jinting Bian, Frank De Boer, Marko Van Eekelen and Stijn De Gouw. Verifying OpenJDK’s LinkedList using KeY
- Alex Dixon and Ranko Lazic. KReach: A Tool for Reachability in Petri Nets
- Roman Kapl and Pavel Parizek. Endicheck: Dynamic Analysis for Detecting Endianness Bugs
- Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis and Christoph Welzel. Structural Invariants for the Verification of Systems with Parameterized Architectures
- Florian Frohn. A Calculus for Modular Loop Acceleration
- Dana Angluin, Dana Fisman and Yaara Shoval. Polynomial Identification of $\omega$-Automata
- Simon Wimmer and Joshua von Mutius. Towards Practical Verification of Reachability Checking for Timed Automata
- Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen and Ufuk Topcu. Scenario-Based Verification of Uncertain MDPs
- Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak. Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning
- Bernardo Almeida, Andreia Mordido and Vasco T. Vasconcelos. Deciding the bisimilarity of context-free session types
- Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann and Mickael Randour. Simple Strategies in Multi-Objective MDPs
- 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
- Miroslav Stankovic, Ezio Bartocci and Laura Kovacs. MORA - Automatic Generation of Moment-Based Invariants
- Umang Mathur, P. Madhusudan and Mahesh Viswanathan. What's Decidable About Program Verification Modulo Axioms?
- Ruben Hamers and Sung-Shik Jongmans. Discourje: Runtime Verification of Communication Protocols in Clojure
- Hussein Sibai, Navid Mokhlesi, Chuchu Fan and Sayan Mitra. Multi-Agent Safety Verification using Symmetry Transformations
- Wenxi Wang, Muhammad Usman, Alyas Almaawi, Kaiyuan Wang, Kuldeep S. Meel and Sarfraz Khurshid. A Study of Symmetry Breaking Predicates and Model Counting
- Naoki Kobayashi, Grigory Fedyukovich and Aarti Gupta. Fold/Unfold Transformations for Fixpoint Logic
- Mirco Giacobbe, Thomas Henzinger and Mathias Lechner. How Many Bits Does it Take to Quantize Your Neural Network?
- Supratik Chakraborty, Ashutosh Gupta and Divyesh Unadkat. Verifying Array Manipulating Programs with Full-Program Induction
- Karl Palmskog, Ahmet Celik and Milos Gligoric. Practical Machine-Checked Formalization of Change Impact Analysis
- Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez and Albert Rubio. GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts
- Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Learning One-Clock Timed Automata
- Juraj Kolčák, Jérémy Dubut, Ichiro Hasuo, Shin-Ya Katsumata, David Sprunger and Akihisa Yamada. Relational Differential Dynamic Logic
- S. Akshay, Paul Gastin, Krishna S and Sparsa Roychoudhary. Revisiting Underapproximate Reachability for Multipushdown Systems
- Richard Bornat, Jaap Boender, Florian Kammueller, Guillaume Poly and Rajagopal Nagarajan. Describing and Simulating Concurrent Quantum Systems