| 2021 | Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible. | Marius Kamp, Michael Philippsen |
| 2021 | GPURepair: Automated Repair of GPU Kernels. | Saurabh Joshi, Gautam Muduganti |
| 2021 | Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). | Andreas Humenberger, Laura Kovcs |
| 2021 | Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching. | Jochen Hoenicke, Tanja Schindler |
| 2021 | Compositional Model Checking for Multi-properties. | Ohad Goudsmid, Orna Grumberg, Sarai Sheinvald |
| 2021 | Model Checking Algorithms for Hyperproperties (Invited Paper). | Bernd Finkbeiner |
| 2021 | Verification of Concurrent Programs Using Petri Net Unfoldings. | Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, Claus Schtzle |
| 2021 | Proving the Existence of Fair Paths in Infinite-State Systems. | Alessandro Cimatti, Alberto Griggio, Enrico Magnago |
| 2021 | Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. | Martin Bromberger, Alberto Fiori, Christoph Weidenbach |
| 2021 | A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries. | Nathalie Bertrand, Marijana Lazic, Josef Widder |
| 2021 | Formal Semantics and Verification of Network-Based Biocomputation Circuits. | Michelle Aluf-Medina, Till Korten, Avraham Raviv, Dan V. Nicolau Jr., Hillel Kugler |
| 2020 | Synthesizing Environment Invariants for Modular Hardware Verification. | Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik |
| 2020 | Generalized Property-Directed Reachability for Hybrid Systems. | Kohei Suenaga, Takuya Ishizawa |
| 2020 | How to Win First-Order Safety Games. | Helmut Seidl, Christian Mller, Bernd Finkbeiner |
| 2020 | Fixing Code that Explodes Under Symbolic Evaluation. | Sorawee Porncharoenwase, James Bornholt, Emina Torlak |
| 2020 | Practical Abstractions for Automated Verification of Shared-Memory Concurrency. | Wytse Oortwijn, Dilian Gurov, Marieke Huisman |
| 2020 | Witnessing Secure Compilation. | Kedar S. Namjoshi, Lucas M. Tabajara |
| 2020 | Systematic Classification of Attackers via Bounded Model Checking. | Eric Rothstein Morris, Jun Sun, Sudipta Chattopadhyay |
| 2020 | Solving $\mathrm {LIA} ^\star $ Using Approximations. | Maxwell Levatich, Nikolaj S. Bjrner, Ruzica Piskac, Sharon Shoham |
| 2020 | Improving Parity Game Solvers with Justifications. | Ruben Lapauw, Maurice Bruynooghe, Marc Denecker |
| 2020 | A Systematic Approach to Abstract Interpretation of Program Transformations. | Sven Keidel, Sebastian Erdweg |
| 2020 | Promptness and Bounded Fairness in Concurrent and Parameterized Systems. | Swen Jacobs, Mouhammad Sakr, Martin Zimmermann |
| 2020 | Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. | Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2020 | Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation. | Oren Ish-Shalom, Shachar Itzhaky, Roman Manevich, Noam Rinetzky |
| 2020 | Cheap CTL Compassion in NuSMV. | Daniel Hausmann, Tadeusz Litak, Christoph Rauch, Matthias Zinner |