Systematic Design of Separation Logics

TL;DR

This paper introduces a systematic methodology for designing separation logics that embed the locality principle by construction, enabling modular heap analysis and broadening the scope of logical systems for program verification.

Contribution

It proposes a parametric, calculational approach to derive local axioms and frame rules for heap-manipulating programs, improving flexibility and applicability over existing methods.

Findings

Derives minimal heap and conditions for heap primitives.

Produces logical systems for correctness and incorrectness analysis.

Designs a novel proof system for inferring necessary preconditions.

Abstract

Thanks to the locality principle, separation logics support modular, scalable analysis of large codebases by relying on local axioms and frame rules to focus only on the heap fragments required for verification. However, depending on the direction (forward vs. backward) and sense of approximation (over vs. under) of the analysis, designing the corresponding proof systems can require some ingenuity. In his work on the calculational design of program logics, Patrick Cousot outlines a methodology for deriving proof systems directly from program semantics using abstract interpretation, covering both correctness and incorrectness analyses. Unfortunately, when applied to heap-manipulating programs, Cousot's calculational approach cannot handle the locality principle, because it does not provide a calculational way to derive frame rules and produces axioms that refer to the global heap. In this paper, we propose a general methodology for systematically deriving local axioms in which the locality principle is embedded by construction. For heap-manipulating primitives, we can derive the minimal required heap and the corresponding pre- and postconditions, complemented by universal frame rules without additional syntactic side conditions. Our method is parametric w.r.t. a set of semantic closure properties that are exploited to design local axioms; it can deal with different memory models; it favors the reuse of many inference rules across over- and under-approximation; and it produces logical systems capable of deriving a broader range of triples w.r.t. existing, cleverly designed, program logics for (in)correctness, ranging from Separation Logic and Incorrectness Separation Logic to Separation Sufficient Incorrectness Logic. Furthermore, we demonstrate the flexibility of our methodology by applying it to design a novel proof system for inferring necessary preconditions with separation logic.