| 2022 | A Flow-Insensitive-Complete Program Representation. | Solne Mirliaz, David Pichardie |
| 2022 | Verifying Pufferfish Privacy in Hidden Markov Models. | Depeng Liu, Bow-Yaw Wang, Lijun Zhang |
| 2022 | Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking. | Peter Gjl Jensen, Jir Srba, Nikolaj Jensen Ulrik, Simon Mejlby Virenfeldt |
| 2022 | Gradient-Descent for Randomized Controllers Under Partial Observability. | Linus Heck, Jip Spel, Sebastian Junges, Joshua Moerman, Joost-Pieter Katoen |
| 2022 | High Assurance Software for Financial Regulation and Business Platforms. | Stephen Goldbaum, Attila Mihly, Tosha Ellison, Earl T. Barr, Mark Marron |
| 2022 | EPMC Gets Knowledge in Multi-agent Systems. | Chen Fu, Ernst Moritz Hahn, Yong Li, Sven Schewe, Meng Sun, Andrea Turrini, Lijun Zhang |
| 2022 | Loop Verification with Invariants and Contracts. | Gidon Ernst |
| 2022 | Fanoos: Multi-resolution, Multi-strength, Interactive Explanations for Learned Systems. | David Bayani, Stefan Mitsch |
| 2022 | Flavors of Sequential Information Flow. | Ezio Bartocci, Thomas Ferrre, Thomas A. Henzinger, Dejan Nickovic, Ana Oliveira da Costa |
| 2022 | Relational String Abstract Domains. | Vincenzo Arceri, Martina Olliaro, Agostino Cortesi, Pietro Ferrara |
| 2021 | Netter: Probabilistic, Stateful Network Models. | Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, Limin Jia |
| 2021 | Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking. | Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2021 | Runtime Abstract Interpretation for Numerical Accuracy and Robustness. | Franck Vdrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles |
| 2021 | Eliminating Message Counters in Synchronous Threshold Automata. | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2021 | Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper). | Bernhard Steffen, Alnis Murtovi |
| 2021 | A Synchronous Effects Logic for Temporal Verification of Pure Esterel. | Yahui Song, Wei-Ngan Chin |
| 2021 | Unbounded Procedure Summaries from Bounded Environments. | Lauren Pick, Grigory Fedyukovich, Aarti Gupta |
| 2021 | Concurrent Correctness in Vector Space. | Christina L. Peterson, Victor Cook, Damian Dechev |
| 2021 | On Preprocessing for Weighted MaxSAT. | Tobias Paxian, Pascal Raiola, Bernd Becker |
| 2021 | Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis. | Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin |
| 2021 | Twinning Automata and Regular Expressions for String Static Analysis. | Luca Negrini, Vincenzo Arceri, Pietro Ferrara, Agostino Cortesi |
| 2021 | A Self-certifying Compilation Framework for WebAssembly. | Kedar S. Namjoshi, Anton Xue |
| 2021 | Compositional Satisfiability Solving in Separation Logic. | Quang Loc Le |
| 2021 | A Design of GPU-Based Quantitative Model Checking. | YoungMin Kwon, Eunhee Kim |
| 2021 | Decomposing Data Structure Commutativity Proofs with $m\!n$-Differencing. | Eric Koskinen, Kshitij Bansal |