2 papers
cs.SE2026
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…
cs.SE2016
Error Invariants for Concurrent Traces
Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei +2
Error invariants are assertions that over-approximate the reachable program states at a given position in an error trace while only capturing states that will still lead to failure…