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}
}