Parma Polyhedra Library 0.11
by Roberto Bagnara, Aug. 16, 2010The Parma Polyhedra Library (PPL) provides numerical abstractions especially targeted at applications in the field of analysis and verification of complex systems. These abstractions include convex polyhedra, defined as the intersection of a finite number of (open or closed) halfspaces, each described by a linear inequality (strict or non-strict) with rational coefficients; some special classes of polyhedra shapes that offer interesting complexity/precision tradeoffs; and grids which represent regularly spaced points that satisfy a set of linear congruence relations. The library also supports finite powersets and products of (any kind of) polyhedra and grids, a mixed integer linear programming problem solver using an exact-arithmetic version of the simplex algorithm, a parametric integer programming solver, and primitives for the termination analysis via the automatic synthesis of linear ranking functions.
We are delighted to announce the availability of PPL 0.11, the latest
release of the Parma Polyhedra Library, a modern library for the
manipulation of convex polyhedra and other numerical abstractions
especially targeted at static analysis and verification of complex
software and hardware systems.
The new release, PPL 0.11, expands the usefulness of the library by
providing new features that should be of interest to people working in
the research fields mentioned above. In particular, the latest
release includes support for:
Parametric Integer Programming (PIP) Problem Solving
====================================================
The new class PIP_Problem provides a Parametric Integer Programming
problem solver (mainly based on P. Feautrier's specification). The
implementation combines a parametric dual simplex algorithm using
exact arithmetic with Gomory's cut generation. This is very useful in
the field of automatic parallelization using the polyhedral model.
"Deterministic" Timeouts Facilities
===================================
It is now possible to set computational bounds (on the library calls
taking exponential time) that do not depend on the actual elapsed time
and hence are independent from the actual computation environment
(CPU, operating system, etc.). This allows, very easily, to code
deterministic algorithms that do attempt to realize a "plan A" and
revert to a "plan B" only in case the original plan proves to be
computationally too expensive.
Automatic Termination Analysis
==============================
The PPL now supports termination analysis via the automatic synthesis
of linear ranking functions. Given a sound approximation of a loop,
the PPL provides methods to decide whether that approximation admits a
linear ranking function (possibly obtaining one as a witness for
termination) and to compute the space of all such functions. In
addition, methods are provided to obtain the space of all linear
quasi-ranking functions, for use in conditional termination analysis.
Approximating Machine Arithmetic
================================
The PPL now provides support for approximating computations involving
(bounded) machine integers. A general wrapping operator is provided
that is parametric with respect to the set of space dimensions
(variables) to be wrapped, the width, representation and overflow
behavior of all these variables. An optional constraint system can,
when given, improve the precision.
This release includes several other enhancements, speed improvements
and some bug fixes.
For more information, visit the PPL web site at
http://www.cs.unipr.it/ppl/
The PPL core development team:
Roberto Bagnara Patricia M. Hill Enea Zaffanella
Applied Formal Methods Laboratory
Department of Mathematics
University of Parma, Italy
