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

Noam Zilberstein, Angelina Saliling, Alexandra Silva

Separation logic's compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges -- many pro…