Parma Polyhedra Library 0.11

Roberto Bagnara <bagnara@cs.unipr.it>
Wed, 4 Aug 2010 08:54:20 -0700 (PDT)

          From comp.compilers

Related articles
Parma Polyhedra Library 0.11 bagnara@cs.unipr.it (Roberto Bagnara) (2010-08-04)
| List of all articles for this month |

From: Roberto Bagnara <bagnara@cs.unipr.it>
Newsgroups: comp.compilers,comp.theory,comp.constraints,sci.math.symbolic
Date: Wed, 4 Aug 2010 08:54:20 -0700 (PDT)
Organization: Compilers Central
Keywords: tools, analysis, available
Posted-Date: 04 Aug 2010 23:35:50 EDT

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


Post a followup to this message

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