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

The compositionality and local reasoning properties of separation logic have led to significant advances in scalable static analysis. But new requirements for program analysis have emerged -- many programs display computational effects (such as randomization) and, orthogonally, static analysis for incorrectness has proved to be very effective. We present Outcome Separation Logic (OSL), the first variant of separation logic that is sound for both correctness and incorrectness reasoning with varying computational effects. OSL has a frame rule that resembles that of standard Separation Logic, however we make different underlying assumptions in order to lift restrictions imposed by SL that preclude reasoning about incorrectness and effects. Building on this fundamental 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 and verification across programs with varying effects.