PPL - BUGSENG (original) (raw)

Trusted Numerical Abstractions for System Verification

The Parma Polyhedra Library (PPL) is a state-of-the-art open-source library developed by BUGSENG for analysis and verification of complex systems. With a strong foundation in formal methods and abstract interpretation, PPL provides a rich set of numerical abstractions that have been widely adopted in academic research and advanced industrial tools.

PPL is designed for developers and researchers who require precise, configurable, and formally sound tools to support their static analysis or model-checking frameworks.

What the PPL Offers

The Parma Polyhedra Library (PPL) provides numerical abstractions especially targeted at applications in the field of analysis and verification of complex systems. These abstractions include convex polyhedra, defined as the intersection of a finite number of (open or closed) halfspaces, each described by a linear inequality (strict or non-strict) with rational coefficients; some special classes of polyhedra shapes that offer interesting complexity/precision tradeoffs; and grids which represent regularly spaced points that satisfy a set of linear congruence relations. The library also supports finite powersets and products of (any kind of) polyhedra and grids, a mixed integer linear programming problem solver using an exact-arithmetic version of the simplex algorithm, a parametric integer programming solver, and primitives for termination analysis via the automatic synthesis of linear ranking functions. (More details are available on the PPL’s internal mechanisms.)

The Parma Polyhedra Library is:

• User friendly (you write x + 2*y + 5*z <= 7 when you mean it)
• Fully dynamic (available virtual memory is the only limitation to the dimension of anything)
• Portable (written in standard C++, with C, Java, Objective CAML, and Prolog interfaces, and following all applicable standards)
• Exception-safe (never leaks resources or leaves invalid object fragments around)
• Efficient (and continuously improved)
• Thoroughly documented
• Free software (distributed under the GNU General Public License version 3 or later)

BPL: The Professional Edition

In addition to the open-source PPL, BUGSENG offers the BUGSENG Polyhedra Library (BPL): a professionally supported and qualified edition of PPL, designed for integration into safety- and security-critical software verification tools.

BPL Highlights:

• Maintained and evolved by the original authors of PPL
• Includes expert-level technical support
• Ideal for industrial-strength verification toolchains and formal methods frameworks
• Folded into the TÜV SÜD Functional Safety Certificate for ECLAIR, ensuring it can be used as part of a certified verification platform in compliance with standards such as IEC 61508, ISO 26262, EN 50128, and others

Looking to integrate BPL into your verification framework or explore how it fits into your safety-critical workflow? Our team is ready to assist with technical and licensing details.