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 (e.g. randomization) and, orthogonally, static analysers must handle incorrectness too. We present Outcome Separation Logic (OSL), a program logic that is sound for both correctness and incorrectness reasoning with varying effects. OSL has a frame rule--just like separation logic--but uses different underlying assumptions that lift restrictions imposed by SL, which precluded reasoning about incorrectness and effects. 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 拥有框架规则——正如分离逻辑——但使用不同的底层假设，解除了分离逻辑施加的限制，这些限制此前排除了对不正确性和效应的推理。基于这一基础理论，我们还定义了使用双分离推导来获取含效应程序规约的符号执行算法。这涉及一种新的三分离推导过程，用于分析因非确定性或概率性选择等效应导致执行分支的程序。本工作通过开启跨两个维度（含不同效应程序中的缺陷检测与验证）更大程度复用分析工具的可能性，进一步推进了分离逻辑所承诺的组合性。