Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects

TL;DR

Outcome Separation Logic (OSL) unifies correctness and incorrectness reasoning for pointer programs with computational effects by integrating heap-based assertions with Outcome Logic and a sound frame rule. The main approach extends OL with separation-logic style frames and develops tri-abduction to compose branches, alongside symbolic execution that reuses correctness summaries for bug finding. Key contributions include a frame-rule soundness proof for multiple effects, tri-abduction and single-path variants, a parametric denotational semantics over Outcome Algebras (deterministic, nondeterministic, probabilistic), and two case studies illustrating bug-finding and reliability analysis. This work enables scalable, tool-friendly analysis by sharing summaries across verification and bug-finding and by handling nondeterministic and probabilistic control flows within a unified framework.

Abstract

Separation logic's compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges -- many programs display computational effects and, orthogonally, static analyzers must handle incorrectness too. We present Outcome Separation Logic (OSL), a program logic that is sound for both correctness and incorrectness reasoning in programs with varying effects. OSL has a frame rule -- just like separation logic -- but uses different underlying assumptions that open up local reasoning to a larger class of properties than can be handled by any single existing logic. Building on this foundational theory, we also define symbolic execution algorithms that use bi-abduction to derive specifications for programs with effects. This involves a new tri-abduction procedure to analyze programs whose execution branches due to effects such as nondeterministic or probabilistic choice. This work furthers the compositionality promised by separation logic by opening up the possibility for greater reuse of analysis tools across two dimensions: bug-finding vs verification in programs with varying effects.

Figures (6)

• Figure 1: Denotational semantics of program commands, parametric on an outcome algebra $\mathcal{A} = \langle A, +, \cdot, \dsser{0}, \dsser{1} \rangle$, an allocator function $\mathsf{alloc} : \mathcal{S}\times \mathcal{H} \to \mathcal{W}_{\mathcal{A}}(\mathsf{Addr})$, and a procedure table $\mathsf{P} \colon \mathsf{Proc} \to \mathsf{Cmd}\times\vec{\mathsf{Var}}$.
• Figure 2: Semantics of outcome assertions given an outcome algebra $\langle A, +, \cdot, \dsser{0},\dsser{1}\rangle$.
• Figure 3: Selected abduction proof rules. Similarly to biab, $B(e_1,e_2)$ represents either $\mathsf{ls}(e_1,e_2)$ or $e_1 \mapsto e_2$. Rules ending in -L have symmetric versions not shown here; see \ref{['fig:triab-pf-full']} for the full proof system.
• Figure 4: Sequencing procedure. The vector $\vec{X}$ is assumed to be fresh and the same size as $\vec{x}$, and $\mathord{\bowtie}\in\{\vee,\oplus\}$.
• Figure 5: Symbolic execution of commands and actions, all logical variables $X,Y\in\mathsf{LVar}$ are assumed to be fresh, $a\in A$ is a program weight, and $b \Coloneqq e_1 = e_2 \mid e_1 \neq e_2$ is a simple test.

Theorems & Definitions (59)

• definition 1: Monoid
• definition 2: Semiring
• definition 3: Outcome Algebra
• definition 4: Deterministic Outcome Algebra
• definition 5: Nondeterministic Outcome Algebra
• definition 6: Probabilistic Outcome Algebra
• definition 7: Outcome Monad
• definition 8: Error Monad Transformer
• definition 9: Outcome Separation Logic Triples
• definition 10: Relation Liftings