News

Here is the news archive is the news archive of the Parma Polyhedra Library.

PPL 0.12.1 has been released

April 16, 2012

This release includes portability improvements, a couple of new minor features, some interface changes and an important bug fix concerning the PIP solver. See the release notes for more information.

New paper to appear on Information and Computation

March 30, 2012

The paper A New Look at the Automatic Synthesis of Linear Ranking Functions has been accepted for publication on Information and Computation The paper presents two algorithms for the synthesis of linear ranking functions that have important applications in automatic termination analysis of computer programs. The algorithms are fully implemented in the Parma Polyhedra Library.

PPL 0.12 has been released

February 27, 2012
This release includes portability improvements, a few bug fixes, and performance improvements for the MIP and PIP solvers. Configurability has also been improved, especially as far as the detection of GMP is concerned. ECLAIR has been introduced into the development workflow to bring the PPL into conformance with the applicable rules in MISRA, CERT, NASA/JPL, ESA/BSSC and other widely-used coding standards. See the release notes for more information.

The PPL has a new logo and web site

November 4, 2011
Thanks to BUGSENG, the Parma Polyhedra Library has a new logo and a completely renovated web site. If you are reading this, you have discovered that the new URI for the PPL is http://bugseng.com/products/ppl.

PPL 0.11.2 has been released

February 27, 2011

This release fixes a few minor bugs of PPL 0.11.1. See the release notes for more information.

PPL 0.11.1 has been released

February 20, 2011

This release includes several important bug fixes and performance improvements. See the release notes for more information.

BUGSENG is the new copyright holder

January 24, 2011

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 .

Two in one shot!

November 17, 2010
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, Dottor2 Bossi and Dottor Poletti!

PPL 0.11 has been released

August 2, 2010
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.

The PPL has now a bug tracking system

June 12, 2009
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.

Elena graduated!

April 27, 2009

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!

PPL 0.10.2 has been released

April 18, 2009
This is a bugfix release. See the release notes for more information.

PPL 0.10.1 has been released

April 14, 2009
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.

New paper on exact join detection

April 11, 2009
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.

PPL development moved to Git

February 22, 2009
PPL development moved away from CVS and now uses the Git distributed version control system. See the PPL Git page for all the details.

New server hosts PPL development

February 10, 2009
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.

Congratulations to Katy Dobson

November 13, 2008
who has been awarded the degree of PhD with the thesis Grid Domains for Analysing Software (supervisor Patricia Hill).

PPL 0.10 has been released

November 10, 2008
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 restructur
Read more »

Possible PPL enhancements at the Graphite Workshop

October 16, 2008

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.

We have a FAQ page, at last

October 4, 2007

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.

PPL 0.9 is now in Fedora 7!

July 12, 2007
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.

New paper on efficiently dealing with integer octagonal constraints

June 1, 2007

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.

Barbara got it!

April 19, 2007

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!

New paper on the applications of polyhedra and related abstractions

January 18, 2007
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.

New paper on the PPL

December 18, 2006
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.

The PPL at the Polyhedral Computation Workshop

May 24, 2006

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.

Andrea got it!

April 26, 2006

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!

PPL 0.9 has been released

March 12, 2006
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.

PPL 0.8 has been released

January 20, 2006
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.
Read more »

New paper on widenings for weakly-relational numeric abstractions

April 13, 2005
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).
Read more »

New research position available

February 18, 2005
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, Italy. 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).

Matthew has joined the team!

February 1, 2005
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.

PPL 0.7 has been released

December 24, 2004
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.
Read more »

PPL position available

November 2, 2004
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.
Read more »

PPL 0.6.1 has been released

August 20, 2004
A few packaging and documentation issues have been fixed. See the release notes for more information.

PPL 0.6 has been released

August 18, 2004
This releases features complete support for powersets of polyhedra, including a powerful and customizable framework for the definition of provably correct widening operators (see Bibliography"]). Another novelty is the support for summary dimensions as proposed in Bibliography"]). 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.

New paper on widenings for powersets domains (including finite sets of polyhedra)

November 7, 2003
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.

A cycle of seminars on convex polyhedra and applications

November 4, 2003
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.

New presentation available

June 18, 2003
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.

PPL 0.5 has been released

April 28, 2003
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.

New paper on convex polyhedra widenings

February 26, 2003
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.
Read more »

PPL 0.4.2 has been released

October 4, 2002
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.

Two new papers on the PPL now available

September 24, 2002
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.

PPL 0.4.1 has been released

July 30, 2002
This is a minor bugfix release. See the release notes for more information.

Elisa got it!

July 23, 2002
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!

PPL 0.4 has been released

July 1, 2002

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). Read more »

New paper on the PPL

June 26, 2002
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.

PPL 0.3 has been released

February 26, 2002

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.

PPL 0.2 has been released

November 14, 2001
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 interpreter.

PPL 0.1 has been released

October 24, 2001
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.