6 citations · 6 across the 5 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…
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…