一句话：提出一种基于分离逻辑的单一规约语言，可同时支持运行时断言检查、性质测试与机器验证证明，并集成到常规开发流程。
系统代码常涉及微妙的所有权与别名关系，传统开发流程中难以灵活使用富规约。本文提出一种基于分离逻辑的单一规约语言，用于刻画系统代码的所有权纪律，并将同一规约无缝用于运行时断言检查、基于性质的测试以及机器可检查的形式证明；这些手段相互补充、相互支撑。作者在具有挑战性的实例上进行了演示：一个生产级 hypervisor 的组件，既以用户态独立运行，也在 hypervisor 中原位集成运行。该工作表明，富规约可以平滑扩展常规软件开发实践，而不仅限于事后或独立的验证活动。
We seek to enable more flexible use of rich specifications in a variety of ways that smoothly extend conventional software development practice. We show how a single specification language, based on separation logic to capture the subtle ownership disciplines of systems code, can be used for runtime assertion checking, for property-based testing, and for formal machine-checked proof—and how each of these complements and supports the others. We demonstrate all this on a challenging example: a component of a production hypervisor, running both stand-alone at user level and in situ in the hypervisor.
@article{paperbot3775,
title = {Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows},
author = {Zain K Aamer and Rini Banerjee and Hiroyuki Katsura and David Kaloper-Meršinjak and Dimitrios J. Economou and Kayvan Memarian and Dhruv Makwana and Neel Krishnaswami and Benjamin C. Pierce and Christopher Pulte and Peter Sewell},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808278}
}