New releases of the Parma Polyhedra Library

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@cs.unipr.it>
            Patricia M. Hill <hill@comp.leeds.ac.uk>
            Enea Zaffanella <zaffanella@cs.unipr.it>


--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara@cs.unipr.it

Return to the comp.compilers page.
Search the comp.compilers archives again.