The core development team is very pleased to announce the availability of PPL 0.9, a new release of the Parma Polyhedra Library.
The key feature of this release is complete support for the domain of rational grids. Roughly speaking, a grid is the solution of a finite system of congruence relations such as `x + y - 2*z = 3 (mod 6)'. Grids can encode information about the patterns of distribution of the values that program variables can take. The implementation offered in PPL 0.9 is, as far as we know, the first published one that is functionally complete (i.e., providing all the required operations, including a provably correct widening) for the purposes of program analysis and verification.
The release includes also many portability improvement and a couple of bug fixes. The precise list of user-visible changes is below. For more information, please come and visit the PPL web site at
On behalf of all the past and present developers listed at http://www.cs.unipr.it/ppl/Credits/ and in the file CREDITS,
Roberto Bagnara bagnara@cs.unipr.it Patricia M. Hill hill@comp.leeds.ac.uk Enea Zaffanella zaffanella@cs.unipr.it
New and Changed Features ========================
o The class Grid provides a complete implementation of the relational domain of rational grids. This can represent all sets that can be expressed by the conjunction of a finite number of congruence relations. 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 such a complete domain is made freely available to the community.
o Several important portability improvements. Among other things, it is now possible to build only the static libraries or only the shared libraries. (Notice that some interfaces depend on the availability of the shared libraries: these will not be built when shared libraries are disabled.)
Bugfixes ========
o Fixed a bug whereby the SICStus Prolog interface could not be built on x86_64.
o Fixed a bug in an internal method that, under some circumstances, could cause a wrong result to be computed.