The Parma Polyhedra Library News

Here is the news archive of the Parma Polyhedra Library.

Feb 27, 2011: PPL 0.11.2 has been released
This release fixes a few minor bugs of PPL 0.11.1. See the release notes for more information.
Feb 20, 2011: PPL 0.11.1 has been released
This release includes several important bug fixes and performance improvements. See the release notes for more information.
Jan 24, 2011: BUGSENG is the new copyright holder
The copyright of the Parma Polyhedra Library has been transferred to BUGSENG a newly established spin-off company of the University of Parma . The PPL will of course continue to be free software, but commercial licensing, support and maintenance is now available from BUGSENG .
Nov 17, 2010: Two in one shot!
Fabio Bossi got a Master’s degree in Computer Science, with full marks and honours and a thesis about the extensions he made to the PPL and to the ECLAIR analyzer in order to support the correct approximation of floating-point computations.
Marco Poletti got a Laurea degree in Computer Science, with full marks and honours and a thesis about his work on the sparse matrices that are used in the MIP and PIP solvers of the PPL.
Congratulations, Dottor² Bossi and Dottor Poletti!
Aug 02, 2010: PPL 0.11 has been released
This release features a brand new Parametric Integer Programming (PIP) problem solver, “deterministic” timeout computation facilities, support for termination analysis via the automatic synthesis of linear ranking functions, support for the approximation of computations involving (bounded) machine integers, plus a number of other new minor features and enhancements, including some speed improvements.
Jun 12, 2009: The PPL has now a bug tracking system
We have finally got round to setting up a bug tracking system for the PPL . Users and developers are now strongly encouraged to use it for communicating, commenting and keeping track of all PPL issues.
Apr 27, 2009: Elena graduated!
Elena Mazzi got her Laurea degree in Mathematics with a dissertation on correct widening operators for weakly-relational numerical abstractions. The widening operators and algorithms described and proved correct in her thesis are the ones used in the BD_Shape and Octagonal_Shape classes of the PPL.
Congratulations, Dottoressa Mazzi!
Apr 18, 2009: PPL 0.10.2 has been released
This is a bugfix release. See the release notes for more information.
Apr 14, 2009: PPL 0.10.1 has been released
This release includes several important improvements to PPL 0.10, among which is better portability (including the support for cross-compilation), increased robustness, better packaging and several bug fixes.
Apr 11, 2009: New paper on exact join detection
Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions presents algorithms to decide whether the lattice-theoretic join of two numerical abstractions (as computed by the upper_bound_assign methods of the PPL) corresponds to set-theoretic union. The algorithms described and proved correct in the paper are the ones actually used in the PPL to implement the upper_bound_assign_if_exact methods.
Feb 22, 2009: PPL development moved to Git
PPL development moved away from CVS and now uses the Git distributed version control system . See the PPL Git page for all the details.
Feb 10, 2009: New server hosts PPL development
AMD Developer Central has donated a bi-quad core machine with the latest AMD Opteron 2384 “Shanghai” processors and 16GB of RAM. The transition of all the PPL data and services from the old (and faulty!) server to the new one has been done mainly thanks to the work of Abramo Bagnara, supported by INRIA. We are extremely grateful to AMD and INRIA for their support.
Nov 13, 2008: Congratulations to Katy Dobson
who has been awarded the degree of PhD with the thesis Grid Domains for Analysing Software (supervisor Patricia Hill ).
Nov 04, 2008: PPL 0.10 has been released
This release, which is under the terms of GPLv3+ , has many new features: more abstractions, including octagonal shapes and boxes; an improved LP solver supporting Mixed Integer (Linear) Programming problems; a more general powerset domain (named Pointset_Powerset) that can be instantiated with any simple PPL domain (not just polyhedra); better foreign language interfaces for C and Prolog, as well as brand new ones for OCaml and Java; an improved and restructured set of documentation manuals; new and more flexible configuration options.
Oct 16, 2008: Possible PPL enhancements at the Graphite Workshop
A Graphite Workshop (Graphite is a framework for high-level loop optimizations on the polyhedral model) is organized on AMD’s campus in Austin, Texas, on November 16 and 17, 2008. Among the topics of the workshop are possible extensions and enhancements of the PPL.
Oct 04, 2007: We have a FAQ page, at last
After more than 5 years of questions (and answers!) we thought we were entitled to have a FAQ page. It is accessible from the choice bar and strip of any page of this site.
Jul 12, 2007: PPL 0.9 is now in Fedora 7!
As part of an ongoing effort to make the Parma Polyhedra Library available (also in binary form) on the major software platforms, version 0.9 of the Parma Polyhedra Library has been packaged to meet the criteria for inclusion in Fedora 7 and is now part of that distribution.
Jun 01, 2007: New paper on efficiently dealing with integer octagonal constraints
An Improved Tight Closure Algorithm for Integer Octagonal Constraints presents and fully justifies a cubic algorithm to compute the tight closure of a set of integer octagonal constraints (a.k.a. UTVPI [Unit Two Variables Per Inequality] integer constraints). The algorithm described in the paper is the one used in the PPL.
Apr 19, 2007: Barbara got it!
Barbara Quartieri got her Laurea degree in Mathematics with a dissertation on efficient closure algorithms for octagonal (a.k.a. single variable per inequality and unit two variables per inequality) constraints (advisers Roberto Bagnara , and Enea Zaffanella ). The best of such algorithms is the one employed in the Octagonal_Shape class of the PPL.
Congratulations, Dottoressa Quartieri!
Jan 18, 2007: New paper on the applications of polyhedra and related abstractions
Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems will tell you several good reasons why libraries like the PPL are developed. It will also tell you some of the difficulties that are on the way to further progress and why the combined effort of people from formal methods, computational geometry and combinatorial optimization is desirable.
Dec 18, 2006: New paper on the PPL
The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems is the first published paper that covers, though not in depth, all the main features of the PPL. It is a very recommended reading for anyone using or considering to use the library.
May 24, 2006: The PPL at the Polyhedral Computation Workshop
The PPL will be presented at the Polyhedral Computation Worskhop, a very interesting event running from October 17th to 20th, 2006, at the Centre de recherches mathématiques, Université de Montréal, Montréal (Québec), Canada.
Apr 26, 2006: Andrea got it!
Andrea Cimino got his Laurea degree in Computer Science with a dissertation on the new PPL’s incremental implementation of the primal simplex algorithm (advisers Enea Zaffanella and Roberto Bagnara ). Despite Andrea’s chaotic nature, the thesis defense was truly brilliant. (A picture is worth a thousand words.)
Well done, Dottor Cimino!
Mar 12, 2006: PPL 0.9 has been released
The key new feature of this release is complete support for rational grids (i.e., solutions of finite systems of congruence relations like x + y - 2*z = 3 (mod 6). The implementation offered in PPL 0.9 is, as far as we know, the first published one that is functionally complete (i.e., providing all the required operations, including a provably correct widening) for the purposes of program analysis and verification. The release includes also many portability improvement and a couple of bug fixes.
Jan 20, 2006: PPL 0.8 has been released
This release has several new features, the two key ones being bounded difference shapes (an improved version of the bounded differences abstraction) and a new class for representing and solving linear programming problems by means of an implementation of the simplex algorithm based on exact arithmetic. Other improvements 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 applications using the library, improvements to the C and Prolog interfaces, and (only) a handful of bug fixes.
Apr 13, 2005: New paper on widenings for weakly-relational numeric abstractions
Widening Operators for Weakly-Relational Numeric Abstractions presents the solution to the problem of defining proper widening operators on several weakly-relational numeric abstractions (including bounded differences and octagons). The proposed solution has the big advantage of allowing the adoption of the semantic versions of the abstract domains, whose elements are geometric shapes, instead of the syntactic domains of constraint networks and matrices (which are more difficult to use and to integrate into analysis tools). The implementation of the proposed widenings relies on the availability of an effective reduction procedure for the considered constraint description: the paper provides such an algorithm for the domain of octagonal shapes. As a bonus, the paper also presents an improvement of the strong closure algorithm defined in [Min01a] that is worth a reduction of the number of additions and comparisons in the range 15-20%, for octagons of dimension greater than 4.
The presented algorithms are already part of the implementation of bounded differences and octagons that will be included in future releases of the PPL.
Feb 18, 2005: New research position available
The position is available for a fixed term of two years to join the Formal Methods research team led by Prof. Roberto Bagnara in the Department of Mathematics , University of Parma . A substantial part of the job concerns the research and development of analysis and verification techniques and tools based on the Parma Polyhedra Library and on PURRS , a system providing sophisticated computer algebra services required by automatic complexity analysis. Enhancements to both the PPL and PURRS are among the results that are expected from this line of work. See the official advert for more information (the deadline for applications is March 18th, 2004).
Feb 01, 2005: Matthew has joined the team!
Matthew Mundell, a member of the Software Analysis research group led by Patricia M. Hill in the School of Computing , University of Leeds , has joined the PPL development team. Matthew will initially focus on the implementation of grid abstractions , but will also help with the general maintenance and development of the library.
Dec 24, 2004: PPL 0.7 has been released
The library can now be configured to use checked native integers (8, 16, 32 or 64 bits wide) as an alternative to the unbounded integer coefficients provided by the GMP library. The checked integer coefficients apply systematic and efficient overflow detection, raising an exception if the computed value cannot be represented by the underlying type. When the numerical coefficients involved are likely to be small, the user can obtain significant efficiency improvements while being sure that, if no exception is thrown, the results are reliable. This release also includes other important improvements ranging from major efficiency gains (for all configurations) to usability and portability. Several bugs have been fixed and a more consistent naming scheme for the library types has been adopted: as a result users willing to upgrade will have to do a little renaming work on their applications. But it is worth the effort. See the release notes for more information.
Nov 02, 2004: PPL position available
The post is available for a fixed term of one year, in the first instance, to join the Software Analysis research team led by Dr Patricia M. Hill in the School of Computing , University of Leeds . A substantial part of the job concerns the development and maintenance of the Parma Polyhedra Library. The ideal candidate should have a good degree in Computer Science or related subject with excellent programming skills and some expertise in C++. See the full advert for more information.
Aug 20, 2004: PPL 0.6.1 has been released
A few packaging and documentation issues have been fixed. See the release notes for more information.
Aug 18, 2004: PPL 0.6 has been released
This releases features complete support for powersets of polyhedra, including a powerful and customizable framework for the definition of provably correct widening operators (see [BHZ03b]). Another novelty is the support for summary dimensions as proposed in [GDD⁺04]). We also have some new demo programs: one of them, ppl_lcdd is competitive with the lcdd_gmp and glrs programs that come with cddlib and lrslib , respectively. There are many other improvements concerning documentation, performance and portability. A handful of bugfixes complete the picture. See the release notes for more information.
Nov 07, 2003: New paper on widenings for powersets domains (including finite sets of polyhedra)
Widening Operators for Powerset Domains deals with the problem of defining widening operators over domains obtained by means of the finite powerset construction, whereby an abstract domain is enhanced in order to represent finite disjunctions of its elements. The general techniques and widenings proposed in the paper are instantiated on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known. The paper will be presented at VMCAI’04 , the Fifth International Conference on Verification, Model Checking and Abstract Interpretation.
Support for powersets of convex polyhedra (with these new widenings) is one of the key new features of the forthcoming release PPL 0.6.
Nov 04, 2003: A cycle of seminars on convex polyhedra and applications
In the coming months, we will have a very interesting cycle of seminars on convex polyhedra for the analysis and verification of hardware and software systems. This will be a nice occasion to get (prospective) developers and (potential) users together and to discuss about the current and future developments.
Jun 18, 2003: New presentation available
The slides of the talk given at SAS’03 have been put online. They provide a good starting point for those interested in the BHRZ03 widening.
Apr 28, 2003: PPL 0.5 has been released
This release is packed with new features: the most precise widening operator on Earth; support for the new widening with tokens technique; several new operations on polyhedra; extended C and Prolog interfaces; many efficiency, usability and portability improvements plus a number of bug fixes. See the release notes for more information.
Feb 26, 2003: New paper on convex polyhedra widenings
Precise Widening Operators for Convex Polyhedra embarks on the challenging task of improving on the standard widening. The paper describes a framework for the systematic definition of widenings that are more precise than the standard one. An instance of the framework is the “BHRZ03” widening, already available in the CVS version and part of the forthcoming PPL 0.5.
A shorter version will be presented at SAS’03 , the 10th Annual International Static Analysis Symposium.
Oct 04, 2002: PPL 0.4.2 has been released
This is a minor bugfix release. Most of these bugs were discovered thanks to the ongoing effort to extend the PPL test suite so as to cover 100% of the library’s code. See the release notes for more information.
Sep 24, 2002: Two new papers on the PPL now available
The first, Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library has been presented at the 9th International Symposium on Static Analysis (SAS’02 , Madrid, Spain, 17-20 September 2002). Slides available.
The second, A New Encoding of Not Necessarily Closed Convex Polyhedra has been presented at the 1st CoLogNet Workshop on Implementation Technology for Computational Logic Systems (ITCLS’02 , Madrid, Spain, 19-20 September 2002). Slides available.
Jul 30, 2002: PPL 0.4.1 has been released
This is a minor bugfix release. See the release notes for more information.
Jul 23, 2002: Elisa got it!
Elisa Ricci got her Laurea degree in Mathematics with a dissertation on the theory of convex polyhedra that the PPL relies upon (advisers Roberto Bagnara , Costantino Medori and Enea Zaffanella ). The thesis defense was brilliant and everyone is happy here.
Congratulations, Dottoressa Ricci!
Jul 01, 2002: PPL 0.4 has been released
This revolutionary release is a big step toward functional completeness of the library. We now have the best available support for Not Necessarily Closed (NNC) polyhedra (that is, polyhedra that can be expressed by a mixture of equalities and strict and non-strict inequalities). A complete C interface has been added and the Prolog interface has been extended and generalized (now supporting GNU Prolog , SICStus Prolog , SWI-Prolog and YAP ). Support has been added for timeout-guarded operations. Portability has also been greatly improved: the library should now be completely written in standard C/C++, compiles cleanly under three major C++ compilers and has been roughly tested on a handful of different computing platforms. Besides that, almost everything has been improved and changed: see the release notes for more information (and forget about any kind of compatibility with release 0.3).
Jun 26, 2002: New paper on the PPL
The paper Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library has been accepted for presentation at SAS’02 (the 9th International Static Analysis Symposium) and inclusion in its proceedings.
Feb 26, 2002: PPL 0.3 has been released
The construction of dynamic libraries is now supported. Switched to the integer C++ class of GMP. New methods for computing convex difference of polyhedra. Some other new methods. Some critical bugs have been fixed. Changed the interface for the limited widening. respectively). Some performance improvements. Added more test programs. See the release notes for more information.
Nov 14, 2001: PPL 0.2 has been released
Massive API changes and greatly improved documentation. All user-accessible library methods are now guarded by suitable sanity checks. A SICStus Prolog interface is now available. It comes with a somewhat interesting demo: a toy CLP(Q) interpreter.
Oct 24, 2001: PPL 0.1 has been released
This is a “shut up and show us the code” release. In other words, it is the very first, very alpha, and only for the brave.