Polyhedral Invariant Generation

The generated invariants have the form l ==> P where l is a location and P is a closed convex polyhedron, that is, a conjunction of inequalities a1.x1 + a2.x2 + ... + an.xn <= b.

The invariants are obtained by running an approximate symbolic computation of the transition system and collecting all the reachable states as a polyhedron. First, a program that maintains a polyhedral variable for each location is extracted. Initial values are computed from the initial state of the transition system. Each transition of the program generates an assignment for the polyhedron corresponding to the post-location of the transition as well as assignments for the polyhedra corresponding to locations of other parallel processes. The program loops until convergence is reached. The approximative nature of the process ensures convergence.

For most of the basic operations over polyhedra the polyhedral manipulation package developed at VERIMAG/CNRS (Grenoble, France) by Nicolas Halbwachs and Yann-Eric Proy with an implementation of the Chernikova algorithm by Herve Leverge, IRISA/INRIA (Rennes, France) is used.

Unfortunately, the time and space used increase dramatically with the number of variables. Therefore we do not recommend its use for more than 20 variables at a time (count local variables of parameterized programs as two). A number of settings can be used to limit its resources, and its operation can be interrupted with the interrupt button.

Additional Arguments

The main algorithms used are described in the following papers:

Back to the STeP home page.