Aaron R. Bradley (Stanford University), Solving Verification Constraint Problems with Constraint Programming

The practice of invariant checking has been helped immensely by the recent interest in making decision procedures practical. It is not unusual for analyses, like predicate abstraction, to make thousands of decision procedure calls. Moreover, these decision queries take full advantage of the range of datatype theories that are practically decidable, including Booleans, reals, linear integers, recursive data structures, and arrays (and their combination).

Invariant generation has also been helped by the recent interest in decision procedures, but not as much. By invariant generation, we mean specifically the synthesis of literals, not the synthesis of Boolean combinations of given literals (as in predicate abstraction). Constraint-based invariant generation, in particular, has exploited fast decision procedures. However, a focus on efficiency through approximation and specialization has resulted in fast but specific invariant generators.

In this talk, we show how techniques from the constraint programming community can be used to reduce invariant generation to invariant checking and ranking function synthesis to ranking function checking. Consequently, we immediately gain the expressiveness of the many decidable theories applied in invariant checking, at the cost of requiring many decision procedure calls. We exhibit the method's effectiveness in several applications.