| 2021 | The Probabilistic Termination Tool Amber. | Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovcs |
| 2021 | From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET. | Anastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger, Michael W. Whalen |
| 2021 | Congruence Relations for Bchi Automata. | Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang |
| 2021 | Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers. | Shankara Narayanan Krishna, Khushraj Madnani, Manuel Mazo Jr., Paritosh K. Pandya |
| 2021 | Formal Analysis of Neural Network-Based Systems in the Aircraft Domain. | Panagiotis Kouvaros, Trent Kyono, Francesco Leofante, Alessio Lomuscio, Dragos D. Margineantu, Denis Osipychev, Yang Zheng |
| 2021 | Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers. | Alexei Kopylov, Stefan Mitsch, Aleksey Nogin, Michael A. Warren |
| 2021 | Trace Abstraction-Based Verification for Uninterpreted Programs. | Weijiang Hong, Zhenbang Chen, Yide Du, Ji Wang |
| 2021 | Combining Forces: How to Formally Verify Informally Defined Embedded Systems. | Paula Herber, Timm Liebrenz, Julius Adelt |
| 2021 | Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives. | Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2021 | Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles. | Rong Gu, Cristina Seceleanu, Eduard Enoiu, Kristina Lundqvist |
| 2021 | Verifying Secure Speculation in Isabelle/HOL. | Matt Griffin, Brijesh Dongol |
| 2021 | HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams. | Felipe Gorostiaga, Csar Snchez |
| 2021 | Formal Verification of Consensus in the Taurus Distributed Database. | Song Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang |
| 2021 | Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. | Simon Foster, Jonathan Julin Huerta y Munive, Mario Gleirscher, Georg Struth |
| 2021 | HyperProb: A Model Checker for Probabilistic Hyperproperties. | Oyendrila Dobe, Erika brahm, Ezio Bartocci, Borzoo Bonakdarpour |
| 2021 | Formal Verification of a JavaCard Virtual Machine with Frama-C. | Adel Djoudi, Martin Hna, Nikolai Kosmatov |
| 2021 | Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models. | Nicholas Coughlin, Kirsten Winter, Graeme Smith |
| 2021 | On Lexicographic Proof Rules for Probabilistic Termination. | Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotn, Jiri Zrevcky, Dorde Zikelic |
| 2021 | Verification of the Incremental Merkle Tree Algorithm with Dafny. | Franck Cassez |
| 2021 | Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers. | Alexandra Bugariu, Arshavir Ter-Gabrielyan, Peter Mller |
| 2021 | Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption. | Frantisek Blahoudek, Murat Cubuktepe, Petr Novotn, Melkior Ornik, Pranay Thangeda, Ufuk Topcu |
| 2021 | Integrating ADTs in KeY and Their Application to History-Based Reasoning. | Jinting Bian, Hans-Dieter A. Hiep, Frank S. de Boer, Stijn de Gouw |
| 2021 | Featured Team Automata. | Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, Jos Proena |
| 2021 | Efficient Algorithms for Omega-Regular Energy Games. | Gal Amram, Shahar Maoz, Or Pistiner, Jan Oliver Ringert |
| 2021 | Formal Verification of Intelligent Hybrid Systems that are Modeled with Simulink and the Reinforcement Learning Toolbox. | Julius Adelt, Timm Liebrenz, Paula Herber |