Parma Polyhedra Library 0.10

roberto.bagnara@gmail.com
Tue, 4 Nov 2008 10:17:51 -0800 (PST)

          From comp.compilers

Related articles
Parma Polyhedra Library 0.10 roberto.bagnara@gmail.com (2008-11-04)
| List of all articles for this month |

From: roberto.bagnara@gmail.com
Newsgroups: comp.compilers
Date: Tue, 4 Nov 2008 10:17:51 -0800 (PST)
Organization: Compilers Central
Keywords: available
Posted-Date: 04 Nov 2008 16:53:16 EST

We are very happy to announce the availability of PPL 0.10, 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.10 --which is under the terms of the GNU General
Public License version 3 (or later)-- 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:


The Domain of Octagonal Shapes
==============================


This is a subdomain of the domain of convex polyhedra providing coarse
but efficient-to-compute approximations for large analysis problems.
It offers greater precision but with a slightly higher time and space
cost compared to that of the domain of "bounded difference shapes"
(BDSs) already provided by the library. As for the BDSs, the domain
of octagonal shapes 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 Domains of Boxes and Intervals
==================================


A "box" represents (geometrically speaking) a not necessarily closed,
iso-oriented hyperrectangle or, if preferred, it can be viewed as the
smash product of `n' not necessarily closed and possibly unbounded
intervals, where `n' is the space dimension of the box. The domain of
such boxes provides computationally efficient and scalable
approximations for program analysis and verification, and is
parametric with respect to a domain of intervals.
A generic implementation of intervals is included in PPL 0.10, which
is parametric on the type used to represent the interval boundaries
(all native integer and floating point types are supported as well as
unbounded integers and rational numbers provided by GMP) and on a
policy that controls whether open boundaries are supported in addition
to closed ones, whether intervals of integers or intervals of reals
are represented, and so forth.


A Mixed Integer Problem Solver
==============================


The class LP_Problem has been renamed MIP_Problem and now supports the
solution of Mixed Integer (Linear) Programming problems. Support has
been added for the incremental solution of MIP problems: it is now
possible to add new space dimensions or new constraints to the
feasible region, as well as change the objective function, the
optimization mode and some control parameters, while still exploiting
some of the computational work done before these changes.


New and Extended Language Interfaces
====================================


New language interfaces have been added for OCaml and Java. Thus the
PPL now supports language interfaces for: C++, C, Java, OCaml, Ciao
Prolog, GNU Prolog, SICStus, SWI-Prolog, XSB and YAP. Most of the
domains provided by the C++ interface and almost all the public
methods for these domains are also supported by all the other
language interfaces.


The release also includes improvements to the documentation, many new
configuration options and a few 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>



Post a followup to this message

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