一句话：提出结果分离逻辑 OSL，统一支持带计算效应的正确性与不正确性推理，并给出符号执行算法。
分离逻辑的合成性与局部推理推动了可扩展静态分析，但现有逻辑难以同时处理计算效应和不正确性推理。本文提出 Outcome Separation Logic (OSL)，一种对带效应程序的正确性与不正确性推理均可靠的程序逻辑。OSL 保留帧规则，但采用不同底层假设，使局部推理能覆盖比任何单一现有逻辑更广的性质。作者进一步定义基于 bi-abduction 的符号执行算法，为带效应程序推导规约，并提出 tri-abduction 以分析因非确定性或概率选择等效应产生的执行分支。该工作从缺陷发现与验证两个维度促进分析工具的复用，扩展了分离逻辑的合成性承诺。
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 displaycomputational effectsand, orthogonally, static analyzers must handleincorrectnesstoo. 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 newtri-abductionprocedure 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.
@article{paperbot2522,
title = {Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects},
author = {Noam Zilberstein and Angelina Saliling and Alexandra Silva},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649821}
}