| 2021 | Apply Formal Methods in Certifying the SyberX High-Assurance Kernel. Wenjing Xu, Yongwang Zhao, Chengtao Cao, Jean Raphael Ngnie Sighom, Lei Wang, Zhe Jiang, Shihong Zou |
| 2021 | BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement Learning. Joseph Scott, Trishal Sudula, Hammad Rehman, Federico Mora, Vijay Ganesh |
| 2021 | Business Processes Meet Spatial Concerns: The sBPMN Verification Framework. Rim Saddem-Yagoubi, Pascal Poizat, Sara Houhou |
| 2021 | Cabean 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks. Cui Su, Jun Pang |
| 2021 | Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon Testbed. Jiawan Wang, Lei Bu, Shaopeng Xing, Yuming Wu, Xuandong Li |
| 2021 | Combining Forces: How to Formally Verify Informally Defined Embedded Systems. Paula Herber, Timm Liebrenz, Julius Adelt |
| 2021 | Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA. Felix A. Wolf, Malte Schwerhoff, Peter Müller |
| 2021 | Congruence Relations for Büchi Automata. Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang |
| 2021 | Divide et Impera: Efficient Synthesis of Cyber-Physical System Architectures from Formal Contracts. César Augusto Ribeiro dos Santos, Tom Schrijvers, Amr Hany Saleh, Mike Nicolai |
| 2021 | Dynamic Reconfiguration via Typed Modalities. Ionut Tutu, Claudia Elena Chirita, José Luiz Fiadeiro |
| 2021 | Efficient Algorithms for Omega-Regular Energy Games. Gal Amram, Shahar Maoz, Or Pistiner, Jan Oliver Ringert |
| 2021 | Featured Team Automata. Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença |
| 2021 | Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning. Andrea Pferscher, Bernhard K. Aichernig |
| 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 | Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings Marieke Huisman, Corina S. Pasareanu, Naijun Zhan |
| 2021 | Formal Verification of Complex Data Paths: An Industrial Experience. Carl-Johan H. Seger |
| 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 | Formal Verification of Intelligent Hybrid Systems that are Modeled with Simulink and the Reinforcement Learning Toolbox. Julius Adelt, Timm Liebrenz, Paula Herber |
| 2021 | Formal Verification of a JavaCard Virtual Machine with Frama-C. Adel Djoudi, Martin Hána, Nikolai Kosmatov |
| 2021 | Formally Guaranteed Tight Dynamic Future Occupancy of Autonomous Vehicles. Yousaf Rahman, Md Tawhid Bin Waez, Yuming Niu |
| 2021 | Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers. Alexei Kopylov, Stefan Mitsch, Aleksey Nogin, Michael A. Warren |
| 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 | Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption. Frantisek Blahoudek, Murat Cubuktepe, Petr Novotný, Melkior Ornik, Pranay Thangeda, Ufuk Topcu |
| 2021 | Gaussian Process-Based Confidence Estimation for Hybrid System Falsification. Zhenya Zhang, Paolo Arcaini |
| 2021 | Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers. Shankara Narayanan Krishna, Khushraj Madnani, Manuel Mazo Jr., Paritosh K. Pandya |
| 2021 | HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams. Felipe Gorostiaga, César Sánchez |
| 2021 | Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study. Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo |
| 2021 | Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth |
| 2021 | HyperProb: A Model Checker for Probabilistic Hyperproperties. Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour |
| 2021 | Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers. Alexandra Bugariu, Arshavir Ter-Gabrielyan, Peter Müller |
| 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 | Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles. Rong Gu, Cristina Seceleanu, Eduard Enoiu, Kristina Lundqvist |
| 2021 | Model Checking for Verification of Quantum Circuits. Mingsheng Ying |
| 2021 | Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives. Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak |
| 2021 | On Lexicographic Proof Rules for Probabilistic Termination. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiri Zárevúcky, Dorde Zikelic |
| 2021 | Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. Daniel Wright, Mark Batty, Brijesh Dongol |
| 2021 | Probabilistic Verification of Neural Networks Against Group Fairness. Bing Sun, Jun Sun, Ting Dai, Lijun Zhang |
| 2021 | Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models. Nicholas Coughlin, Kirsten Winter, Graeme Smith |
| 2021 | Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms. Grant Olney Passmore |
| 2021 | The Probabilistic Termination Tool Amber. Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács |
| 2021 | Trace Abstraction-Based Verification for Uninterpreted Programs. Weijiang Hong, Zhenbang Chen, Yide Du, Ji Wang |
| 2021 | Two Decades of Formal Methods in Industrial Products at BTC Embedded Systems. Tino Teige, Andreas Eggers, Karsten Scheibler, Matthias Stasch, Udo Brockmeyer, Hans Jürgen Holberg, Tom Bienmüller |
| 2021 | Two Mechanisations of WebAssembly 1.0. Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner |
| 2021 | Verification of the Incremental Merkle Tree Algorithm with Dafny. Franck Cassez |
| 2021 | Verified Quadratic Virtual Substitution for Real Arithmetic. Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer |
| 2021 | Verifying Secure Speculation in Isabelle/HOL. Matt Griffin, Brijesh Dongol |
| 2021 | Z3str4: A Multi-armed String Solver. Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka, Vijay Ganesh |