2 papers
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…
cs.PL2024
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…