Zohar Manna (Stanford University), From Verification Conditions to Constraints

Checking if an assertion is an inductive program invariant requires checking the validity of verification conditions. Similarly, checking if a function is a ranking function requires checking the validity of verification conditions. Except for the assertion/function, the verification conditions are generated from the text of the transition system. Thus, these verification conditions can be seen as constraints on the assertion or function. Checking the validity of verification conditions for a particular assertion/function is akin to checking whether constraints are satisfied by a particular value. Replacing the proposed assertion/function by a parameterized expression lifts the problem to constraint solving, where the constraints are generated entirely from the transition system, and a solution (an assignment to the parameters) provides an inductive assertion/ranking function.

The constraint-based approach to invariant generation and ranking function synthesis exploits this perspective. We have used this approach to solve previously unsolved problems such as generating polynomial invariants and generating invariants/ranking functions of integer loops in a theoretically complete way. We have also used the approach to produce theoretically and practically efficient invariant generation and ranking function synthesis algorithms for the linear case, where abstract interpretation over polyhedra is usually applied.

In this talk, we first review recent work on the constraint-based approach. We then present a method for solving more general constraint problems. It combines techniques from the numerical constraint solving community with decision procedures. The resulting algorithm takes as input a parameterized formula and a hyper-rectangle over which the parameters range; it returns the integer instantiations of the parameters that validate the formula. The formula can contain arbitrary quantification and theories, as long as validity of the formula under any integer instantiation is decidable. We illustrate the constraint-based method and the constraint-solving procedure on several examples, including invariant generation of polynomial inequality invariants over nonlinear loops, synthesis of barrier certificates in continuous systems, and reachability analysis of hybrid systems.