What question did this study set out to answer?

The aim is to integrate rich specifications using separation logic into standard software development workflows.

June 10, 2026Open Access

Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows

ZAZain K AamerCalifornia University of Pennsylvania RBRini BanerjeeUniversity of Cambridge HKHiroyuki KatsuraUniversity of Cambridge

Key Points

The aim is to integrate rich specifications using separation logic into standard software development workflows.
Developed a specification language based on separation logic for various applications.
Applied the specification language for runtime assertion checking, property-based testing, and formal proof.
Tested the approach using a component of a production hypervisor.
Presented evidence of effective runtime assertion checking using separation logic.
Outlined successful property-based testing outcomes that leverage specifications.
Showed the feasibility of formal machine-checked proof in complementing the other methods.

Abstract

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.

KI fragen

Bookmark

View Full Paper