2 papers
cs.PL2026
Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions
Wannes Tas, Bart Jacobs
The Rust programming language is famous for its strong ownership regime: at each point, each value is either exclusively owned, exclusively borrowed through a mutable reference, or…
cs.PL2025
An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model
Bart Jacobs, Justus Fasse
We propose an approach for modular verification of programs that use relaxed-consistency atomic memory access primitives and fences. The approach is sufficient for verifying the co…