We present a technique for using infeasible program paths to find predicates describing properties of unbounded arrays. First, we use specialized axioms for reasoning about arrays to build proofs of unsatisfiability for the infeasible program paths. Next, we compute interpolants from the proof that describe abstract program configurations that are both precise enough to refute the path, and, given enough paths, general enough to prove the program safe. By embedding the technique within a Counterexample-Guided Abstraction-Refinement (CEGAR) loop, we obtain a method for verifying data-sensitive safety properties whose precision is tailored in a program- and property-sensitive manner. Though the axioms used are simple, we show the method suffices to prove a variety of array-manipulating programs that were previously beyond the scope of automatic software model checkers.
Proceedings of the 19th Intl. Conference on Computer-Aided Verification (CAV), 2007 (to appear).