一句话：通过欠指定扩展 Incorrectness Logic，使其支持反向推理，并证明可靠性与部分完备性，且在 Isabelle/HOL 中形式化。
本文研究 O’Hearn 的 incorrectness logic（IL）的一个扩展，目标是使其支持反向推理。现有 IL 通常不能通用地进行反向推理；作者提出通过引入欠指定（underspecification）来缓解这一问题。扩展后的逻辑同时具备两项特征：后置条件（结果）只需对相关变量给出约束，且保持欠近似，从而聚焦于少于全部的执行路径。作者证明了该证明系统的可靠性，并针对一类所定义的 presumption 证明了完备性。文中还讨论了从给定 result 推导 presumption 的证明策略，并表明循环摘要（loop summaries）这一闭式符号表示对反向推理十分有用。该逻辑、证明系统及全部定理均已在 Isabelle/HOL 定理证明器中形式化。
This paper studies an extension of O’Hearn’s incorrectness logic (IL) that allows backwards reasoning. IL in its current form does not generically permit backwards reasoning. We show t at this can be mitigated by extending IL with underspecification. The resulting logic combines underspecification (the result, or postcondition, only needs to formulate constraints over relevant variables) with underapproximation (it allows to focus on fewer than all the paths). We prove soundness of the proof system, as well as completeness for a defined subset of presumptions. We discuss proof strategies that allow one to derive a presumption from a given result. Notably, we show that the existing concept of loop summaries- closed-form symbolic representations that summarize the effects of executing an entire loop at once- is highly useful. The logic, the proof system and all theorems have been formalized in the Isabelle/HOL theorem prover.
@article{VerbeekSFR25,
title = {On Extending Incorrectness Logic with Backwards Reasoning},
author = {Freek Verbeek and Md Syadus Sefat and Zhoulai Fu and Binoy Ravindran},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704850}
}