Parma Polyhedra Library 0.11
in [Theory]
|
Prev: A simple template for writing multiprograms; will it work always?
Next: Last CFP - Applied Computing 2010: 3 September 2010
From: Roberto Bagnara on 4 Aug 2010 11:54 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 |