VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs

By: Bart Jacobs

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 and to some recent proposals for Iris-like reasoning without the later modality.

Keywords

Separation Logic, Fine-Grained Concurrency, Modular Verification

Cite as:

Bart Jacobs, “VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs”, Journal of Object Technology, Volume 25, no. 1 ( 2026), pp. 1:1-10, doi:10.5381/jot.2026.25.1.a4.

DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn