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, as Outcome Logic can do too. 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. 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能比不正确性分离逻辑生成更简洁的后置条件，提供更强的保证，并支持有效的反向推理。