| 2022 | Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols. | Joonwon Choi, Adam Chlipala, Arvind |
| 2022 | Does a Program Yield the Right Distribution? - Verifying Probabilistic Programs via Generating Functions. | Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler |
| 2022 | Proof-Guided Underapproximation Widening for Bounded Model Checking. | Prantik Chatterjee, Jaydeepsinh Meda, Akash Lal, Subhajit Roy |
| 2022 | Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs. | Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Dorde Zikelic |
| 2022 | Multi: A Formal Playground for Multi-Smart Contract Interaction. | Martn Ceresa, Csar Snchez |
| 2022 | Playing Against Fair Adversaries in Stochastic Games with Total Rewards. | Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi, Luciano Putruele |
| 2022 | Neural Network Robustness as a Verification Property: A Principled Case Study. | Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, Idan Refaeli |
| 2022 | Local Search for SMT on Linear Integer Arithmetic. | Shaowei Cai, Bohan Li, Xindi Zhang |
| 2022 | Proofgold: Blockchain for Formal Methods. | Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban |
| 2022 | Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes. | Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl |
| 2022 | Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations. | Michael Blondin, Filip Mazowiecki, Philip Offtermatt |
| 2022 | Software Verification of Hyperproperties Beyond k-Safety. | Raven Beutner, Bernd Finkbeiner |
| 2022 | Formal Specification for Learning-Enabled Autonomous Systems. | Saddek Bensalem, Chih-Hong Cheng, Xiaowei Huang, Panagiotis Katsaros, Adam Molin, Dejan Nickovic, Doron Peled |
| 2022 | Abstraction Modulo Stability for Reverse Engineering. | Anna Becchi, Alessandro Cimatti |
| 2022 | MEV-Freedom, in DeFi and Beyond (Invited Talk). | Massimo Bartoletti |
| 2022 | Data-Driven Invariant Learning for Probabilistic Programs. | Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, Subhajit Roy |
| 2022 | Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption. | Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga, Kohei Suenaga |
| 2022 | SMT-Based Translation Validation for Machine Learning Compiler. | Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo, Juneyoung Lee |
| 2022 | Automatic Generation of Attacker Contracts in Solidity. | Ignacio Ballesteros, Clara Benac Earle, Luis Eduardo Bueso de Barrio, Lars-ke Fredlund, ngel Herranz, Julio Mario |
| 2022 | Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement. | Stanley Bak, Sergiy Bogomolov, Brandon Hencey, Niklas Kochdumper, Ethan Lew, Kostiantyn Potomkin |
| 2022 | Sampling-Based Verification of CTMCs with Uncertain Rates. | Thom S. Badings, Nils Jansen, Sebastian Junges, Marille Stoelinga, Matthias Volk |
| 2022 | SolCMC: Solidity Compiler's Model Checker. | Leonardo Alt, Martin Blicha, Antti E. J. Hyvrinen, Natasha Sharygina |
| 2022 | Distilling Constraints in Zero-Knowledge Protocols. | Elvira Albert, Marta Bells-Muoz, Miguel Isabel, Clara Rodrguez-Nez, Albert Rubio |
| 2022 | PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP. | Chaitanya Agarwal, Shibashis Guha, Jan Kretnsk, Pazhamalai Muruganandham |
| 2021 | Reflections on Termination of Linear Loops. | Shaowei Zhu, Zachary Kincaid |