Academy News

Here is the news archive of the Academy partnership.

Next generation static software analysis tools

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

New paper to be presented at PPDP 2013

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.

New paper to be presented at ICST 2013

The paper Symbolic Path-Oriented Test Data Generation for Floating-Point Programs has been accepted for presentation at the 6th IEEE International Conference on Software Testing, Verification and Validation. The paper presents novel techniques that allow to automatically reason about and generate tests for programs that engage into floating-point intensive computations, a problem that is notoriously quite difficult and insidious.

PPL 0.12 has been released

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.

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

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.

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!

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.

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.

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 flexi

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.

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.

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.

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

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

Widening Operator 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.

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.

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

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

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.

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.

We are a passionate team of experts. Do not hesitate to let us have your feedback:
You may be surprised to discover just how much your suggestions matter to us.