一句话：提出后向欠近似的 SIL 与 Separation SIL 证明系统，定位错误来源并处理指针与动态内存错误。
可靠过近似方法能证明程序无错，但会产生误报；欠近似方法面向缺陷检测，不产生误报，却需要定位错误来源。本文提出两个通过后向欠近似定位错误来源的证明系统：Sufficient Incorrectness Logic (SIL) 及其面向内存错误的特化 Separation SIL。SIL 是最小且对 Lisbon 三元组可靠、完备的系统，可用于从否定、近似方向、执行顺序和分析目标等维度比较基于三元组的程序逻辑。Separation SIL 是其核心扩展，为涉及指针和动态内存分配的程序提供自动后向推理，具有可靠性并相对完备；该完备性依赖断言语言与原子命令规则的精心设计。
Sound over-approximation methods are effective for proving the absence of errors, but inevitably produce false alarms that can hamper programmers. In contrast, under-approximation methods focus on bug detection and are free from false alarms. In this work, we present two novel proof systems designed to locate the source of errors via backward under-approximation, namely Sufficient Incorrectness Logic (SIL) and its specialization for handling memory errors, called Separation SIL. The SIL proof system is minimal, sound and complete for Lisbon triples, enabling a detailed comparison of triple-based program logics across various dimensions, including negation, approximation, execution order, and analysis objectives. More importantly, SIL lays the foundation for our main technical contribution, by distilling the inference rules of Separation SIL, a sound and (relatively) complete proof system for automated backward reasoning in programs involving pointers and dynamic memory allocation. The completeness result for Separation SIL relies on a careful crafting of both the assertion language and the rules for atomic commands.
@article{paperbot3161,
title = {Revealing Sources of (Memory) Errors via Backward Analysis},
author = {Flavio Ascari and Roberto Bruni and Roberta Gori and Francesco Logozzo},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720486}
}