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.

翻译：由于局部性原则，分离逻辑通过依赖局部公理和框架规则，仅聚焦验证所需的堆片段，从而支持对大型代码库进行模块化、可扩展的分析。然而，根据分析的方向（前向 vs. 后向）和近似性质（超 vs. 欠），设计相应的证明系统可能需要一定的独创性。在关于程序逻辑演算化设计的著作中，Patrick Cousot 概述了一种利用抽象解释直接从程序语义推导证明系统的方法，涵盖了正确性与不正确性分析。遗憾的是，当应用于堆操作程序时，Cousot 的演算化方法无法处理局部性原则，因为它既不能提供推导框架规则的演算途径，又会产生引用全局堆的公理。本文提出了一种通用方法，用于系统化地推导嵌入了局部性原则的局部公理。对于堆操作原语，我们可推导出所需的最小堆及其对应的前置条件和后置条件，并辅以无需额外语法侧条件的通用框架规则。该方法以一组语义闭包性质为参数，这些性质被用于设计局部公理；它能处理不同的内存模型；有助于在超近似和欠近似分析中复用众多推理规则；并能生成推导范围更广的三元组的逻辑系统，其能力超越现有精巧设计的（不）正确性程序逻辑，涵盖从分离逻辑、不正确性分离逻辑到分离充分不正确性逻辑。此外，我们通过应用该方法设计一种基于分离逻辑推导必要前置条件的新型证明系统，展示了其灵活性。