Academy News

Our CEO and CTO will attend the invitation-only Dagstuhl Seminar 14352: Next Generation Static Software Analysis Tools. This seminar brings together developers of software analysis tools and algorithms, including researchers working on the underlying decision procedures (e.g., SMT solvers), and people who are interested in applying these techniques (e.g., in the automotive or avionics industry).

The paper Eventual Linear Ranking Functions has been accepted for presentation at the 15th International Symposium on Principles and Practice of Declarative Programming. The paper introduces the concept of eventual linear ranking function (ELRF), i.e., a linear function that becomes a ranking functions after a finite unrolling of the loop, and present an algorithm that decides the existence of ELRFs for a certain class of loops.

BUGSENG personnel is involved in several 2013 international conferences and symposia that have, among their key topics, methodologies, techniques and tools to (automatically) reason about programs.

This release includes support for the optimized representation of sparse vectors of coefficients, achieving significant performance improvements, e.g., when dealing with constraint systems describing weakly relational abstractions such as boxes and octagonal shapes. See the release notes for more information.

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.

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.

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

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!

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.

This is a bugfix release. See the release notes for more information.

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.

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.

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 flexi

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.

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.

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.Well done, Dottor Cimino!

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.

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.

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++.

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]).

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.

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.

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.

This is a minor bugfix release. See the release notes for more information.

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).

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.