Sound over-approximation methods have been proved effective for guaranteeing the absence of errors, but inevitably they produce false alarms that can hamper the programmers. Conversely, under-approximation methods are aimed at bug finding and are free from false alarms. We introduce Sufficient Incorrectness Logic~(SIL), a new under-approximating, triple-based program logic to reason about program errors. SIL is designed to set apart the initial states leading to errors. We prove that SIL is correct and complete for a minimal set of rules, and we study additional rules that can facilitate program analyses. We formally compare SIL to existing triple-based program logics. Incorrectness Logic and SIL both perform under-approximations, but while the former exposes only true errors, the latter locates the set of initial states that lead to such errors. Hoare Logic performs over-approximations and as such cannot capture the set of initial states leading to errors in nondeterministic programs -- for deterministic and terminating programs, Hoare Logic and SIL coincide. Finally, we instantiate SIL with Separation Logic formulae (Separation SIL) to handle pointers and dynamic allocation and we prove its correctness and, for loop-free programs, also its completeness. We argue that in some cases Separation SIL can yield more succinct postconditions and provide stronger guarantees than Incorrectness Separation Logic and can support effective backward reasoning.

翻译：抽象：可靠的过近似方法已被证明在保证程序无错误方面有效，但不可避免地会产生可能妨碍程序员的误报。相反，欠近似方法旨在发现错误且无误报。我们引入充分不正确性逻辑（SIL），一种新的基于三元组的欠近似程序逻辑，用于推理程序错误。SIL旨在区分导致错误的初始状态。我们证明SIL在最小规则集下是正确且完备的，并研究了可促进程序分析的附加规则。我们将SIL与现有的基于三元组的程序逻辑进行了形式化比较。不正确性逻辑和SIL都执行欠近似，但前者仅揭示真实错误，而后者定位导致这些错误的初始状态集合。霍尔逻辑执行过近似，因此无法捕获非确定性程序中导致错误的初始状态集合——对于确定性和终止程序，霍尔逻辑与SIL一致。最后，我们用分离逻辑公式实例化SIL（分离SIL），以处理指针和动态分配，并证明其正确性，对于无循环程序还证明了其完备性。我们认为，在某些情况下，分离SIL相比不正确性分离逻辑能生成更简洁的后置条件，提供更强的保证，并支持有效的反向推理。