Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)
summary
Outcome Separation Logic gives a single formalism that proves both correctness and incorrectness for programs with effects by making postconditions talk about sets of reachable outcomes rather than single states and adding a separation logic frame rule to distribute context across outcomes. The implementation shows symbolic execution with bi-abduction extended to a new tri-abduction procedure with three unknowns, enabling single-pass analysis of branching effects and handling nondeterministic and probabilistic choice. The OSL algorithms integrate with tools like Infer and derive both full and underapproximate specs.
AI-written summary · about
chapters (11)
- 0:00Outcome separation logic intro
- 1:23Bugs and incorrectness logic
- 3:29Outcome triples and reachable states
- 5:59Specifying bugs with outcome logic
- 7:04Case study: Infer and Pulse
- 8:51Compositionality in separation logic
- 10:38Abduction and frame rule
- 11:40Triabduction for branching
- 13:06Algorithms for correctness/incorrectness
- 14:33Conclusion and future work
- 15:15Q&A
related talks
20mTotal Outcome Logic: Termination and Nontermination Proving for Effectful Branching
25mA Relational Separation Logic for Effect Handlers
17mCalculational design of Incorrectness Separation Logic
05mNew foundations for probabilistic separation logic
22mImplementing separation logic using an SMT-backed Frame Rule
29mLogical Relations for Effect Capabilities
19mBeyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
16mGradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification