首页|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
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.点此复制
评论