| 2021 | cake_lpr: Verified Propagation Redundancy Checking in CakeML. | Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen |
| 2021 | Finding Provably Optimal Markov Chains. | Jip Spel, Sebastian Junges, Joost-Pieter Katoen |
| 2021 | SyReNN: A Tool for Analyzing Deep Neural Networks. | Matthew Sotoudeh, Aditya V. Thakur |
| 2021 | Network Traffic Classification by Program Synthesis. | Lei Shi, Yahui Li, Boon Thau Loo, Rajeev Alur |
| 2021 | Towards String Support in JayHorn (Competition Contribution). | Ali Shamakhi, Hossein Hojjat, Philipp Rmmer |
| 2021 | MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. | Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh |
| 2021 | Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints - (Competition Contribution). | Simmo Saan, Michael Schwarz, Kalmer Apinis, Julian Erhard, Helmut Seidl, Ralf Vogler, Vesal Vojdani |
| 2021 | Making Theory Reasoning Simpler. | Giles Reger, Johannes Schoisswohl, Andrei Voronkov |
| 2021 | Multi-objective Optimization of Long-run Average and Total Rewards. | Tim Quatmann, Joost-Pieter Katoen |
| 2021 | Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models. | Andrea Peruffo, Daniele Ahmed, Alessandro Abate |
| 2021 | SAT Solving with GPU Accelerated Inprocessing. | Muhammad Osama, Anton Wijs, Armin Biere |
| 2021 | Syntax-Guided Quantifier Instantiation. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution). | Malte Mues, Falk Howar |
| 2021 | Certifying Proofs in the First-Order Theory of Rewriting. | Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer |
| 2021 | Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes. | Fabian Meyer, Marcel Hark, Jrgen Giesl |
| 2021 | Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. | Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett |
| 2021 | Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring. | Konstantinos Mamouras, Agnishom Chattopadhyay, Zhifu Wang |
| 2021 | General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond. | Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche |
| 2021 | A Two-Phase Approach for Conditional Floating-Point Verification. | Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis |
| 2021 | Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities. | Julien Lepiller, Ruzica Piskac, Martin Schf, Mark Santolucito |
| 2021 | Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution). | Hernn Ponce de Len, Thomas Haas, Roland Meyer |
| 2021 | Momba: JANI Meets Python. | Maximilian A. Khl, Michaela Klauck, Holger Hermanns |
| 2021 | AMulet 2.0 for Verifying Multiplier Circuits. | Daniela Kaufmann, Armin Biere |
| 2021 | Bounded Model Checking for Hyperproperties. | Tzu-Han Hsu, Csar Snchez, Borzoo Bonakdarpour |
| 2021 | HLola: a Very Functional Tool for Extensible Stream Runtime Verification. | Felipe Gorostiaga, Csar Snchez |