|国家预印本平台
首页|VeriFast's separation logic: a higher-order(ish) logic without laters for modular verification of fine-grained concurrent programs

VeriFast's separation logic: a higher-order(ish) logic without laters for modular verification of fine-grained concurrent programs

VeriFast's separation logic: a higher-order(ish) logic without laters for modular verification of fine-grained concurrent programs

来源:Arxiv_logoArxiv
英文摘要

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 a later modality. We present the first formalization and soundness proof for this aspect of VeriFast's logic.

Bart Jacobs

计算技术、计算机技术

Bart Jacobs.VeriFast's separation logic: a higher-order(ish) logic without laters for modular verification of fine-grained concurrent programs[EB/OL].(2025-05-07)[2025-07-02].https://arxiv.org/abs/2505.04500.点此复制

评论