| 2021 | A Web Interface for Petri Nets with Transits and Petri Games. | Manuel Gieseking, Jesko Hecking-Harbusch, Ann Yanich |
| 2021 | FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions. | Margarida Ferreira, Miguel Terra-Neves, Miguel Ventura, Ins Lynce, Ruben Martins |
| 2021 | Bridging Arrays and ADTs in Recursive Proofs. | Grigory Fedyukovich, Gidon Ernst |
| 2021 | VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution). | Priyanka Darke, Sakshi Agrawal, R. Venkatesh |
| 2021 | Local Search with a SAT Oracle for Combinatorial Optimization. | Aviad Cohen, Alexander Nadel, Vadim Ryvchin |
| 2021 | Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution). | Marek Chalupa, Toms Jasek, Jakub Novk, Anna Rechtckov, Veronika Sokov, Jan Strejcek |
| 2021 | Replicating sc Restart with Prolonged Retrials: An Experimental Report. | Carlos E. Budde, Arnd Hartmanns |
| 2021 | Generating Extended Resolution Proofs with a BDD-Based SAT Solver. | Randal E. Bryant, Marijn J. H. Heule |
| 2021 | Directed Reachability for Infinite-State Systems. | Michael Blondin, Christoph Haase, Philip Offtermatt |
| 2021 | A Game for Linear-time-Branching-time Spectroscopy. | Benjamin Bisping, Uwe Nestmann |
| 2021 | RTLola on Board: Testing Real Driving Emissions on your Phone. | Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian A. Khl, Yannik Schnitzer, Maximilian Schwenger |
| 2021 | Symbolic Coloured SCC Decomposition. | Nikola Benes, Lubos Brim, Samuel Pastva, David Safrnek |
| 2021 | Timed Automata Relaxation for Reachability. | Jaroslav Bendk, Ahmet Sencan, Ebru Aydin Gol, Ivana Cern |
| 2021 | On Satisficing in Quantitative Games. | Suguman Bansal, Krishnendu Chatterjee, Moshe Y. Vardi |
| 2021 | A Flexible Proof Format for SAT Solver-Elaborator Communication. | Seulkee Baek, Mario Carneiro, Marijn J. H. Heule |
| 2021 | Analysis of Markov Jump Processes under Terminal Constraints. | Michael Backenkhler, Luca Bortolussi, Gerrit Gromann, Verena Wolf |
| 2021 | dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts. | Pranav Ashok, Mathias Jackermeier, Jan Kretnsk, Christoph Weinhuber, Maximilian Weininger, Mayank Yadav |
| 2021 | Inductive Synthesis for Probabilistic Programs Reaches New Horizons. | Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen |
| 2021 | cpalockator: Thread-Modular Analysis with Projections - (Competition Contribution). | Pavel S. Andrianov, Vadim S. Mutilin, Alexey V. Khoroshilov |
| 2021 | Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata. | tienne Andr, Jaime Arias, Laure Petrucci, Jaco van de Pol |
| 2021 | An SMT-Based Approach for Verifying Binarized Neural Networks. | Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2021 | Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution). | Zsfia dm, Gyula Sallai, kos Hajdu |
| 2021 | Deductive Verification of Floating-Point Java Programs in KeY. | Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt |
| 2021 | Resilient Capacity-Aware Routing. | Stefan Schmid, Nicolas Schnepf, Jir Srba |
| 2021 | Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. | Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi |