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.

翻译：分离逻辑的组合性和局部推理特性推动了可扩展静态分析的显著进步。然而，程序分析的新需求已经出现——许多程序表现出计算效应（如随机化），并且正交地，面向错误性的静态分析已被证明非常有效。我们提出了结果分离逻辑（OSL），这是首个对涉及不同计算效应的正确性和错误性推理均保持健全性的分离逻辑变体。OSL具有类似于标准分离逻辑的框架规则，但我们做出了不同的底层假设，以消除分离逻辑施加的、阻碍错误性和效应推理的限制。基于这一基础理论，我们还定义了使用双溯因来推导含效应程序规约的符号执行算法。这涉及一种新的三溯因过程，用于分析因非确定性或概率性选择等效应导致执行分支的程序。本工作通过开辟分析工具在两个维度上（跨不同效应的程序的缺陷查找和验证）实现更大程度复用的可能性，进一步推动了分离逻辑所承诺的组合性。