Incorrectness Proofs with Underapproximation Invariants

Incorrectness logic provides a theoretical framework to reason about program faults. While incorrectness logic has been immensely successful at explaining bug-finding tools, automating incorrectness logic, especially its backwards variant rule has remained challenging. The tools based on incorrectness logic, instead, analyze bounded models of a program using a loop unrolling rule that unrolls loops to finite bounds. While such analysis via loop unrolling is quite effective for shallow bugs, discovering deep bugs remains a challenge. In this work, we propose a new proof system, \ (I3\), that, instead of requiring backwards variants, allows partial incorrectness proofs with a new kind of invariant, the underapproximation invariant. Unlike regular invariants that must hold on all program traces, underapproximation invariants are required to hold only on a subset of traces. We also show that, under certain sufficient conditions, a partial incorrectness proof does guarantee total incorrectness. Given the success of invariant inference in automating partial correctness proofs with Floyd-Hoare logic, we believe that \ (I3\) should also be easier to automate. We implement our proof system within a prover, I3Prove, that is able to automatically infer suitable underapproximation invariants en route to incorrectness proofs. We compare I3Prove against leading bug-finding tools from the SV-COMP23 competition, viz. UAutomizer, CPAChecker, and Veriabs. We also compare it with a recent proposal, Banal, that uses abstract interpretation to reason about incorrectness claims. On our benchmark suite of 106 incorrect programs, I3Prove is able to prove the incorrectness claims in 97 programs, while the best of the baseline tools is only able to solve 69 instances.