Property Checking Without Inductive Invariants
Eugene Goldberg
TL;DR
This paper introduces ProveProp, a PQE-based framework for proving safety properties without generating inductive invariants. It reduces property checking to the Reachability Diameter (RD) problem and bad-state reachability, solved via Partial Quantifier Elimination, enabling depth-first search to uncover deep bugs while avoiding exhaustive state enumeration. A key contribution is proving a property or finding a counterexample without constructing a strong inductive invariant, and a variant, ProveProp*, expands the initial state set to accelerate convergence. The approach offers practical benefits for complex hardware verification tasks where invariants are large or difficult to obtain, and it integrates neatly with existing PQE-based techniques to provide complete, DFS-enabled verification with potentially faster outcomes.
Abstract
We introduce a procedure for proving safety properties. This procedure is based on a technique called Partial Quantifier Elimination (PQE). In contrast to complete quantifier elimination, in PQE, only a part of the formula is taken out of the scope of quantifiers. So, PQE can be dramatically more efficient than complete quantifier elimination. The appeal of our procedure is twofold. First, it can prove a property without generating an inductive invariant. Second, it employs depth-first search and so can be used to find deep bugs.