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.

翻译：分离逻辑的组成性与局部推理特性推动了可扩展静态分析的显著进展。然而程序分析面临新挑战——许多程序展现出计算效应，且静态分析器还需处理程序错误。我们提出结果分离逻辑（OSL），这是一种在具有不同效应的程序中既能进行正确性推理也能进行错误性推理的程序逻辑。OSL拥有帧规则——如同分离逻辑——但采用不同的底层假设，使得局部推理能够处理比任何单一现有逻辑更广的属性类别。基于这一基础理论，我们还定义了使用双溯因推导含效应程序规约的符号执行算法。这涉及一种新的三溯因过程，用于分析因非确定性或概率选择等效应导致执行分支的程序。本工作通过开辟在具有不同效应的程序中沿错误检测与验证两个维度复用分析工具的可能性，进一步推进了分离逻辑所承诺的组成性。