VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs.
Abstract
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 its support for expressively specifying fine-grained concurrent modules, without the need for the later modality.We present the first formalization and soundness proof for this aspect of VeriFast's logic, and we compare it both to Iris, a state-of-the-art logic for fine-grained concurrency which features the later modality, as well as to some recent proposals for Iris-like reasoning without the later modality.
Fields of Study & Subjects
Logic
programming
and type systems
Formal Methods in Verification
Software Testing and Debugging Techniques
Publication details
- Journal / source
- The Journal of Object Technology
- Volume
- 25
- Issue
- 1
- Pages
- 1:1–1:1
- Publication date
- 1 January 2026
- Language
- EN