一句话：提出 Fulminate，将带 CN 分离逻辑前后条件的 C 代码翻译为运行时检查代码，实现所有权测试。
分离逻辑已成为形式化刻画与推理命令式程序所有权模式的重要工具，既用于纸笔证明，也支撑工业静态分析与多个证明工具。然而，在具体执行中对分离逻辑规约进行程序测试的工作却很少。分离逻辑公式带有对堆分割的隐式量化及其他存在量化，直接求值通常难以在合理时间内完成。本文观察到，CN 证明工具为获得可预测证明自动化而采用的受限分离逻辑片段，同时具有自然且可读的计算解释，因而可在运行时测试中实际使用。作者据此设计并实现了从 C + CN 源码到 C 源码的翻译器 Fulminate，为带有 CN 前后条件的 C 代码插入所有权检查与所有权转移检查，并在非平凡示例上进行了演示，包括某生产级 hypervisor 中的分配器。作者还形式化了其运行时所有权测试方案，在一个小型类 C 语言语义中展示并证明了具体化的 ghost state 如何正确刻画所有权传递。
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 separationlogic 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.
@article{BanerjeeMMPKS25,
title = {Fulminate: Testing CN Separation-Logic Specifications in C},
author = {Rini Banerjee and Kayvan Memarian and Dhruv Makwana and Christopher Pulte and Neel Krishnaswami and Peter Sewell},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704879}
}