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拥有框架规则——如同分离逻辑——但使用不同的底层假设，从而将局部推理扩展到比任何单一现有逻辑所能处理更广泛的属性类别。基于这一基础理论，我们还定义了符号执行算法，该算法利用双溯因推导具有效应的程序的规约。这涉及一种新的三溯因过程，用于分析因非确定性或概率选择等效应而产生执行分支的程序。本研究进一步推进了分离逻辑所承诺的组合性，通过开辟跨两个维度（具有不同效应程序中的错误查找与验证）更大程度复用分析工具的可能性。