Here is the news archive of the Academy partnership.
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).
This release includes support for positive time elapse, a new operator on polyhedra, improvements to the Java interface, several portability improvements and a few bug fixes. See the release notes for more information.
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.
Roberto Bagnara will give an invited talk at the 13th International Conference on Quality Software (QSIC 2013), July 29-30, 2013 in Nanjing, China. The QSIC series of conferences has a long tradition of bringing together researchers and practitioners to present and discuss innovative methods of assuring software and system qualities.
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.
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.
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.
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.
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!
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.
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 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
Octagonal_Shape classes of the PPL.Congratulations, Dottoressa Mazzi!
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.
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
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.
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.
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.
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.
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.
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).
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 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.
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++.
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.
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.
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.
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.
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).
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 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.
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.
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.
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.