Publications (7)
Predicate Abstraction via Symbolic Decision Procedures
Shuvendu K. Lahiri, Thomas Ball, Byron Cook
We present a new approach for performing predicate abstraction based on symbolic decision procedures. Intuitively, a symbolic decision procedure for a theory takes a set of predica…
T2: Temporal Property Verification
Marc Brockschmidt, Byron Cook, Samin Ishtiaq +2
We present the open-source tool T2, the first public release from the TERMINATOR project. T2 has been extended over the past decade to support automatic temporal-logic proving tech…
Verifying the Rust Standard Library
Byron Cook, Remi Delmas, Zyad Hassan +9
Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic…
A Neurosymbolic Approach to Natural Language Formalization and Verification
Chenyang An, Sam Bayless, Stefano Buliani +27
The paper presents ARc, a system that combines large language models with automated reasoning to formally translate natural‑language policies and verify their logical correctness,…
Spatial Interpolants
Aws Albarghouthi, Josh Berdine, Byron Cook +1
We propose Splinter, a new technique for proving properties of heap-manipulating programs that marries (1) a new separation logic-based analysis for heap reasoning with (2) an inte…
Learning How to Cube
Ferhat Erata, Sam Kouteili, Thanos Typaldos +4
Despite the effectiveness of Cube-and-Conquer (C&C) for solving challenging Boolean Satisfiability (SAT) problems, no prior work has shown that transformer-based models can learn e…
Partitioning Strategies for Distributed SMT Solving
Amalee Wilson, Andres Noetzli, Andrew Reynolds +3
For many users of Satisfiability Modulo Theories (SMT) solvers, the solver's performance is the main bottleneck in their application. One promising approach for improving performan…