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
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.
- 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.
Back to the STeP home page.