# New releases of the Parma Polyhedra Library

*From*: "Roberto Bagnara" <bagnara@xxxxxxxxxxx>*Date*: 13 Mar 2006 01:11:31 -0800

We are very happy to announce the availability of PPL 0.9, 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.

Besides improving upon almost all of the functionality available since

the release of PPL 0.7 in December 2004, the two recent releases of

PPL 0.8 and PPL 0.9 have expanded the usefulness of the library by

providing new features that should be of great interest to people

working in the research fields mentioned above. In particular, the

latest release includes support for:

The Domain of Relational Rational Grids

=======================================

The class Grid can represent and manipulate the set of solutions of a

finite conjunction of congruence relations. Elements of this domain

can thus be used to encode information about the patterns of

distribution of the values that program variables can take.

Operations provided include everything that is needed in the field of

static analysis and verification, including affine images, preimages

and their generalizations, grid-difference and widening operators.

This is the first time that one of the most precise variants of the

domain initially proposed by P. Granger is made freely available to

the community. Moreover, as the PPL provides several polyhedral

domains as well as full support for lifting any domain to the powerset

of that domain, a user of the library can now experiment with the

extra precision provided by abstract domain constructions and

combinations including not only Z-polyhedra, but also grid-polyhedra,

grid-bounded-differences and their powersets.

The Domain of Bounded Difference Shapes

=======================================

This is a subdomain of the domain of convex polyhedra providing coarse

but efficient-to-compute approximations for large analysis problems.

The domain can be instantiated to use a wide range of different data

types, including exact arithmetic rationals or integers, bounded

precision floating point data types with controlled rounding and

bounded integer data types with systematic yet efficient overflow

detection. The full set of operations needed for static analysis and

verification are supported, here included the semantic widening

operator defined in our SAS 2005 paper.

A Linear Programming Solver Based on Exact Arithmetic

=====================================================

The class LP_Problem can be used to represent, check the

satisfiability and optimize linear programming problems. The solver

is based on a primal simplex algorithm using exact arithmetic.

Other enhancements include a new configuration program and Autoconf

function making library usage even easier; several new operations

useful for static analyzers; new output methods for debugging;

improvements to the C and Prolog interfaces; several important

portability improvements; and (only) a handful of bug fixes.

For more information, visit the PPL web site at

http://www.cs.unipr.it/ppl/

The PPL core development team:

Roberto Bagnara <bagnara@xxxxxxxxxxx>

Patricia M. Hill <hill@xxxxxxxxxxxxxxxx>

Enea Zaffanella <zaffanella@xxxxxxxxxxx>

--

Prof. Roberto Bagnara

Computer Science Group

Department of Mathematics, University of Parma, Italy

http://www.cs.unipr.it/~bagnara/

mailto:bagnara@xxxxxxxxxxx

.

- Prev by Date:
**quick math competition for anyone interested** - Next by Date:
**Macsyma: sin(x)/cos(x) = tan(x)** - Previous by thread:
**quick math competition for anyone interested** - Next by thread:
**Macsyma: sin(x)/cos(x) = tan(x)** - Index(es):