# 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.

• Degree of precision
A parameter that controls the number of exact (in the polyhedra domain) initial iterations in the symbolic computation of the set of reachable states. Sometimes, this can result in stronger invariants. The convergence process, on the other hand, is slowed down.
Default: 0
• Variables to be ignored
A set of variables to be ignored by the polyhedra invariant generator. Variables that have no bearing on a given goal can be listed here. Alternatively, the set of variables can be partitioned into subsets of semantically related variables and the polyhedra invariant generator can be invoked separetly for each subset.
Default: No variable is ignored
• Location variables to be considered
The invariants generated when considering location variables can sometimes be useful. This is the case with mutual exclusion properties.
Default: No location variable is considered.

The main algorithms used are described in the following papers:

• N. V. Chernikova, "Algorithm for Discovering the Set of all Solutions of a Linear Programming Problem", U.S.S.R. Computational Mathematics and Mathematical Physics, 8(6), pages 282-293, 1968.
• P. Cousot, N. Halbwachs, "Automatic Discovery of Linear Restraints among Variables of a Program", In 5th ACM Symposium on Principles of Programming Languages, Tucson, Arizona, pages 84-97, 1978.