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

TL;DR

This paper formalizes VeriFast's separation logic, which supports modular verification of fine-grained concurrent programs without using the later modality, and compares it to Iris and other recent approaches.

Contribution

It provides the first formalization and soundness proof for VeriFast's logic that omits the later modality, enabling simpler reasoning about concurrent modules.

Findings

Formalization and proof of soundness for VeriFast's logic without later modality

Comparison with Iris logic highlighting differences and advantages

Insights into reasoning about fine-grained concurrency without the later modality

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.