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.

翻译：VeriFast是半自动化模块化形式化程序验证领域的领先工具之一。其核心特性在于支持高阶幽灵代码，这使得它能够无需later模态即可对细粒度并发模块进行富有表达力的规约。本文首次对该逻辑的这一方面进行了形式化处理并给出了可靠性证明，同时将其与采用later模态的细粒度并发前沿逻辑Iris，以及近期提出的若干类Iris无later模态推理方案进行了对比分析。