Wed, 4 Aug 2010 08:54:20 -0700 (PDT)

Related articles |
---|

Parma Polyhedra Library 0.11 bagnara@cs.unipr.it (Roberto Bagnara) (2010-08-04) |

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.