Reference. Fulminate: Testing CN Separation-Logic Specifications in C
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.
Cite
Cited by (1)
Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows aamer-2026-code
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.
Cites 54 works (3 here)
With notes (3)
CN: Verifying Systems C Code with Separation-Logic Refinement Types pulte-2023-cn
Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability. We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google’s pKVM hypervisor for Android.
Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
Separation logic: A logic for shared mutable data structures reynolds_separation_2002
In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.
External (51)
- Separation Logic Foundations. Software Foundations (2024)
- The VeriFast Program Verifier: A Tutorial (2024)
- VST-A: A Foundationally Sound Annotation Verifier (2024)
- Supplementary material for Fulminate: Testing CN Separation-Logic Specifications in C (2024)
- Verifiable C. Software Foundations (2023)
- Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion Checking (2023)
- The Cerberus C semantics (Tech. Report UCAM-CL-TR-981) (2023)
- The Prusti Project: Formal Verification for Rust (2022)
- Finding real bugs in big programs with incorrectness logic (2022)
- Gillian, Part II: Real-World Verification for JavaScript and C (2021)
- RefinedC: automating the foundational verification of C code with refined ownership types (2021)
- The e-ACSL perspective on runtime assertion checking (2021)
- Gillian, part i: a multi-language platform for symbolic execution (2020)
- Virtualisation for the Masses: Exposing KVM on Android (KVM Forum slides) (2020)
- Virtualization for the Masses: Exposing KVM on Android (talk video) (2020)
- Stacked borrows: an aliasing model for Rust (2019)
- Exploring C semantics and pointer provenance (2019)
- VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs (2018)
- E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper) (2018)
- From Static Analysis to Runtime Verification with Frama-C and E-ACSL (habilitation) (2018)
- Efficient Incrementalized Runtime Checking of Linear Measures on Lists (2017)
- Viper: A Verification Infrastructure for Permission-Based Reasoning (2017)
- Destination-passing style for efficient memory management (2017)
- Model checking for symbolic-heap separation logic with inductive predicates (2016)
- Integrated Environment for Diagnosing Verification Errors (2016)
- Static versus Dynamic Verification in Why3, Frama-C and SPARK (2016)
- Into the depths of C: elaborating the de facto standards (2016)
- Your Proof Fails? Testing Helps to Find the Reason (2016)
- Mechanized verification of fine-grained concurrent programs (2015)
- MemorySanitizer: Fast detector of uninitialized memory use in C++ (2015)
- Sound Modular Verification of C Code Executing in an Unverified Context (2014)
- Instrumentation of Annotated C Programs for Test Generation (2014)
- Common specification language for static and dynamic analysis of C programs (2013)
- Behavioral interface specification languages (2012)
- Recursive proofs for inductive tree data-structures (2012)
- AddressSanitizer: A Fast Address Sanity Checker (2012)
- Implicit dynamic frames (2012)
- Infer: An Automatic Program Verifier for Memory Safety of C Programs (2011)
- VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java (2011)
- Using Debuggers to Understand Failed Verification Attempts (2011)
- Linear Logic and Imperative Programming (PhD thesis) (2008)
- Compiling pattern matching to good decision trees (2008)
- Runtime Checking for Separation Logic (2008)
- Liquid types (2008)
- DITTO: automatic incrementalization of data structure invariant checks (in Java) (2007)
- Expressing heap-shape contracts in linear logic (2006)
- Monadic concurrent linear logic programming (2005)
- How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification (2003)
- Computability and Complexity Results for a Spatial Assertion Language for Data Structures (2001)
- An Overview of Anna, a Specification Language for Ada (1985)
- Report on the programming language Euclid (1977)