# Parma Polyhedra Library 0.11

The 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