| 2020 | Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification. | Jack J. Garzella, Marek S. Baranowski, Shaobo He, Zvonimir Rakamaric |
| 2020 | BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results. | Pietro Ferrara, Luca Olivieri, Fausto Spoto |
| 2020 | Language Inclusion for Finite Prime Event Structures. | Andreas Fellner, Thorsten Tarrach, Georg Weissenbacher |
| 2020 | The Correctness of a Code Generator for a Functional Language. | Nathanal Courant, Antoine Sr, Natarajan Shankar |
| 2020 | Sharing Ghost Variables in a Collection of Abstract Domains. | Marc Chevalier, Jrme Feret |
| 2020 | Formalizing and Checking Multilevel Consistency. | Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Ranjal Gautham Shenoy, S. P. Suresh |
| 2020 | A Cooperative Parallelization Approach for Property-Directed k-Induction. | Martin Blicha, Antti E. J. Hyvrinen, Matteo Marescotti, Natasha Sharygina |
| 2019 | Application of Abstract Interpretation to the Automotive Electronic Control System. | Tomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, Yoshiumi Kawamura |
| 2019 | Program Synthesis with Equivalence Reduction. | Calvin Smith, Aws Albarghouthi |
| 2019 | On the Semantics of Snapshot Isolation. | Azalea Raad, Ori Lahav, Viktor Vafeiadis |
| 2019 | A Decidable Logic for Tree Data-Structures with Measurements. | Xiaokang Qiu, Yanjun Wang |
| 2019 | Mechanically Proving Determinacy of Hierarchical Block Diagram Translations. | Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis |
| 2019 | Effect-Driven Flow Analysis. | Jens Nicolay, Quentin Stivenart, Wolfgang De Meuter, Coen De Roover |
| 2019 | Automatic Program Repair Using Formal Verification and Expression Templates. | Thanh-Toan Nguyen, Quang-Trung Ta, Wei-Ngan Chin |
| 2019 | A Practical Algorithm for Structure Embedding. | Charlie Murphy, Zachary Kincaid |
| 2019 | Type-Directed Bounding of Collections in Reactive Programs. | Tianhan Lu, Pavol Cern, Bor-Yuh Evan Chang, Ashutosh Trivedi |
| 2019 | Fast BGP Simulation of Large Datacenters. | Nuno P. Lopes, Andrey Rybalchenko |
| 2019 | Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs. | Anja F. Karl, Robert Schilling, Roderick Bloem, Stefan Mangard |
| 2019 | A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization. | Richard Huybers, Alfons Laarman |
| 2019 | Solving and Interpolating Constant Arrays Based on Weak Equivalences. | Jochen Hoenicke, Tanja Schindler |
| 2019 | Minimal Synthesis of String to String Functions from Examples. | Jad Hamza, Viktor Kuncak |
| 2019 | Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics. | Stefan Haar, Juraj Kolck, Loc Paulev |
| 2019 | Relatively Complete Pushdown Analysis of Escape Continuations. | Kimball Germane, Matthew Might |
| 2019 | Demand Control-Flow Analysis. | Kimball Germane, Jay McCarthy, Michael D. Adams, Matthew Might |
| 2019 | Termination of Nondeterministic Probabilistic Programs. | Hongfei Fu, Krishnendu Chatterjee |