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能生成比错误分离逻辑更简洁的后置条件，提供更强保障，并支持高效的反向推理。