Showing cs.PLShow all
2 papers · 1 filter
cs.PL2026
Foundational VeriFast: Pragmatic Certification of Verification Tool Results through Hinted Mirroring
Bart Jacobs
VeriFast is a leading tool for the modular formal verification of correctness properties of single-threaded and multi-threaded C and Rust programs. It verifies a program by symboli…
cs.PL2025
VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs
Bart Jacobs
VeriFast is one of the leading tools for semi-automated modular formal program verification. A central feature of VeriFast is its support for higher-order ghost code, which enables…