3 citations · 7 across the 10 of their papers we have counts for
4 papers · 1 filter
Kani: A Model Checker for Rust
Rémi Delmas, Zyad Hassan, Qinheping Hu +9
Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw p…
Teaching LLMs Program Semantics via Symbolic Execution Traces
Jonas Bayer, Stefan Zetzsche, Olivier Bouissou +3
We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025,…
CBMC: The C Bounded Model Checker
Daniel Kroening, Peter Schrammel, Michael Tautschnig
The C Bounded Model Checker (CBMC) demonstrates the violation of assertions in C programs, or proves safety of the assertions under a given bound. CBMC implements a bit-precise tra…
Assisted Coverage Closure
Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy +3
The malfunction of safety-critical systems may cause damage to people and the environment. Software within those systems is rigorously designed and verified according to domain spe…