1 citations · 1 across the 6 of their papers we have counts for
6 papers
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…
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…
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…
A flexible specification approach for verifying total correctness of fine-grained concurrent modules
Justus Fasse, Bart Jacobs
A well-established approach to proving progress properties such as deadlock-freedom and termination is to associate obligations with threads. For example, in most existing work the…
Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract)
Tobias Reinhard, Justus Fasse, Bart Jacobs
Bounded proofs are convenient to use due to the high degree of automation that exhaustive checking affords. However, they fall short of providing the robust assurances offered by u…
Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report
Tobias Reinhard
In this early technical report on an ongoing project, we present -- to the best of our knowledge -- the first study of completeness thresholds for memory safety proofs. Specificall…