Fulminate: Testing CN Separation-Logic Specifications in C

作     者：Banerjee, Rini Memarian, Kayvan Makwana, Dhruv Pulte, Christopher Krishnaswami, Neel Sewell, Peter 

作者机构：Univ Cambridge Cambridge England 

出 版 物：《PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL》 (Proc. ACM Program. Lang.)

年 卷 期：2025年第9卷第POPL期

页      面：1260-1292页

核心收录：

基　　金：UKRI European Resarch Council 

主　　题：C verification separation logic refinement types runtime testing pKVM Android 

摘      要：Separation logic has become an important tool for formally capturing and reasoning about the ownership patterns of imperative programs, originally for paper proof, and now the foundation for industrial static analyses and multiple proof tools. However, there has been very little work on program testing of separation- logic specifications in concrete execution. At first sight, separation-logic formulas are hard to evaluate in reasonable time, with their implicit quantification over heap splittings, and other explicit existentials. In this paper we observe that a restricted fragment of separation logic, adopted in the CN proof tool to enable predictable proof automation, also has a natural and readable computational interpretation, that makes it practically usable in runtime testing. We discuss various design issues and develop this as a C+CN source to C source translation, Fulminate. This adds checks - including ownership checks and ownership transfer - for C code annotated with CN pre- and post-conditions;we demonstrate this on nontrivial examples, including the allocator from a production hypervisor. We formalise our runtime ownership testing scheme, showing (and proving) how its reified ghost state correctly captures ownership passing, in a semantics for a small C-like language.