activity
20162026
most citedBounded Model Checking of State-Space Digital Systems: The Impact of Finite Word-Length Effects on the Implementation of Fixed-Point Digital Controllers Based on State-Space Modeling

4 citations · 5 across the 7 of their papers we have counts for

collaborators
Showing cs.LOShow all

2 papers · 1 filter

cs.LO2026

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…

cs.LO2019

Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space

Mikhail R. Gadelha, Felipe R. Monteiro, Enrico Steffinlongo +2

We describe and evaluate a novel k-induction proof rule called bidirectional k-induction (bkind), which substantially improves the k-induction bug-finding capabilities. Particularl…