| 2025 | Bounded-Exhaustive Subspace Diversification for SMT Solver Testing. | Junda Zheng, Peisen Yao |
| 2025 | Enhancing Neural Network Robustness via Synthesis of Repair Programs. | Tom Yuviler, Dana Drachsler-Cohen |
| 2025 | Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell. | Bram Vandenbogaerde, Sarah Verbelen, Noah Van Es, Coen De Roover |
| 2025 | Abstracting Concolic Execution for Soft Contract Verification. | Bram Vandenbogaerde, Quentin Stivenart, Coen De Roover |
| 2025 | Specifying and Verifying Future Conditions. | Yahui Song, Darius Foo, Wei-Ngan Chin |
| 2025 | Comparing the Precision of Abstract Operators in the eBPF Verifier Using Differential Synthesis. | Matan Shachnai, Harishankar Vishwanathan, Srinivas Narayana, Santosh Nagarakatte |
| 2025 | Verifying Neural Networks with PyRAT. | Augustin Lemesle, Julien Lehmann, Tristan Le Gall, Zakaria Chihani |
| 2025 | Formal Analysis of Networked PLC Controllers Interacting with Physical Environments. | Jaeseo Lee, Kyungmin Bae |
| 2025 | Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types. | Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato |
| 2025 | AURA: Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty. | Zixin Huang, Jacob Laurel, Saikat Dutta, Sasa Misailovic |
| 2025 | Ductape: Optimizing Dynamically Typed Programs Using Ahead-of-Time Compilation and Data-Flow Analysis. | Adi Harif, Shachar Itzhaky |
| 2025 | Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters. | Noah Van Es, Bram Vandenbogaerde, Coen De Roover |
| 2025 | Contextual Equality Saturation. | Alexandre Drewery, Thomas P. Jensen, David Pichardie |
| 2025 | On a Simple Problem Due to Yves Bertot. | Olivier Danvy |
| 2025 | A Programming Language for Feasible Solutions. | Weijun Chen, Yuxi Fu, Huan Long |
| 2025 | Relating Distances and Abstractions - An Abstract Interpretation Perspective. | Marco Campion, Isabella Mastroeni, Caterina Urban |
| 2024 | Verifying Components of Arm | Tong Wu, Shale Xiong, Edoardo Manino, Gareth Stockwell, Lucas C. Cordeiro |
| 2024 | BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code. | Ian Smith |
| 2024 | ConstraintFlow: A Declarative DSL for Easy Development of DNN Certifiers. | Avaljot Singh, Yasmin Sarita, Charith Mendis, Gagandeep Singh |
| 2024 | Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel. | Matan Shachnai, Harishankar Vishwanathan, Srinivas Narayana, Santosh Nagarakatte |
| 2024 | An Order Theory Framework of Recurrence Equations for Static Cost Analysis - Dynamic Inference of Non-Linear Inequality Invariants. | Louis Rustenholz, Pedro Lpez-Garca, Jos F. Morales, Manuel V. Hermenegildo |
| 2024 | Robustness Verification of Multi-label Neural Network Classifiers. | Julian Mour, Dana Drachsler-Cohen |
| 2024 | Under-Approximating Memory Abstractions. | Marco Milanese, Antoine Min |
| 2024 | Quantitative Static Timing Analysis. | Denis Mazzucato, Marco Campion, Caterina Urban |
| 2024 | Verification of Programs with ADTs Using Shallow Horn Clauses. | Tho Losekoot, Thomas Genet, Thomas P. Jensen |