Documentation of the Parma Polyhedra Library

You can find here all the existing documentation for the latest release of the Parma Polyhedra Library. Please, let us know of any inaccuracies.

If you are looking for the documentation of another release or development snapshot or if you want to rebuild the documentation, just follow the instructions.

Jump to: user documentation, developer documentation, presentations, bibliographies, licences.

PPL Documentation for Users

The PPL user’s manual contains all the information you need to use the library and nothing else. This means that we have tried to conceal the implementation details as much as possible. This manual also contains a brief introduction to convex polyhedra and to their double representation.

By keeping clear of the implementation details (e.g., by not looking at the PPL include file, ppl.hh) you can reduce the risks that future releases of the library will break your code. This is a general and obvious truth. However, until version 1.0 of the library is released, we cannot promise that the API will not change, even though stabilization is already in progress and we are rather satisfied about the current interfaces. Please be patient and do not hesitate to contact us to let us know your thoughts about how the API should evolve.

The user’s manuals are available in several formats, suitable for either printing or browsing on a computer screen. Besides the core library documentation, describing the semantic domains, their operators and the templatic C++ language interface, we also provide manuals for each of the non-templatic language interfaces. These come in two versions: a configuration independent version, providing a fixed reference, and a configuration dependent version, whose contents vary according to the set of domain instantiation that have been made available at library configuration time (here below we provide the documentation generated when using configuration option --enable-instantiations=all).

PPL User Documentation
Format Core Library Non-Templatic Language Interfaces
Configuration Independent Configuration Dependent On-line browsing C++ C Java OCaml Prolog C Java OCaml Prolog HTML C++ C Java OCaml Prolog C Java OCaml Prolog PDF C++ C Java OCaml Prolog C Java OCaml Prolog PostScript C++ C Java OCaml Prolog C Java OCaml Prolog

PPL Documentation for Developers

The PPL developer’s manual reveals everything about the implementation of the library. It is meant both for developers and for people that want to know more about the inner workings. Users wishing to help us debugging the library may also find it useful.

We are trying to write the best possible documentation and you will find that the PPL is extensively documented. The developer’s manual includes the mathematical definitions and results needed to help you understand as well as in justifying the algorithms and data structures used in the implementation.

PPL Developer Documentation
Format Core Library Non-Templatic Language Interfaces
Configuration Independent Configuration Dependent On-line browsing C++ C Java OCaml Prolog C Java OCaml Prolog HTML C++ C Java OCaml Prolog C Java OCaml Prolog PDF C++ C Java OCaml Prolog C Java OCaml Prolog PostScript C++ C Java OCaml Prolog C Java OCaml Prolog

Presentations of or About the PPL

The Parma Polyhedra Library: seminar given by Roberto Bagnara at the Département de Mathématiques et Informatique in St Denis de La Réunion, France, Indian Ocean, on May 22nd, 2002. Transparencies available in PostScript and PDF.
Presentation of the paper Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library given by Enea Zaffanella at the 9th International Symposium on Static Analysis (SAS’02 ), in Madrid, Spain, on September 18th, 2002. Transparencies available in PostScript and PDF.
Presentation of the paper A New Encoding of Not Necessarily Closed Convex Polyhedra given by Roberto Bagnara at the 1st CoLogNet Workshop on Implementation Technology for Computational Logic Systems (PostScript ,%0A%20%20%20%20in%20Madrid,%20Spain,%0A%20%20%20%20on%20September%2020th,%202002.%0A%20%20%20%20Transparencies%20available%0A%20%20%20%20in%20%3CA%20HREF=){ppl_talk_itcls_2002.ps.gz”=""} and PDF.
Presentation of the paper Precise Widening Operators for Convex Polyhedra given by Roberto Bagnara at the 10th International Symposium on Static Analysis (SAS’03 ), in San Diego, California, USA, on June 13th, 2003. Transparencies available in PostScript and PDF.
Convex Polyhedra for the Analysis and Verification of Hardware and Software Systems: the “Parma Polyhedra Library”: seminar given by Roberto Bagnara at the Dipartimento di Matematica in Parma, Italy, on December 11th, 2003. Transparencies available in PostScript and PDF.
New Widening Operators for Convex Polyhedra: seminar given by Enea Zaffanella at the Dipartimento di Matematica in Parma, Italy, on December 11th, 2003. Transparencies available in PostScript and PDF.
Representation and Manipulation of Not Necessarily Closed Convex Polyhedra: seminar given by Roberto Bagnara at the Dipartimento di Matematica in Parma, Italy, on February 26th, 2004. Transparencies available in PostScript and PDF.
Widenings for Powerset Domains with Applications to Finite Sets of Polyhedra: seminar given by Enea Zaffanella at the Dipartimento di Matematica in Parma, Italy, on February 26th, 2004. Transparencies available in PostScript and PDF.
The PPL: A Library for Representing Numerical Abstractions: Current and Future Plans: seminar given by Patricia Hill at the School of Computing in Leeds, UK, on June 28th, 2004. (A version of this talk was presented by Roberto Bagnara at the CoVer3 Workshop .) Transparencies available in PostScript and PDF.
Abstract Interpretation and the PPL: From Theory to Practice and Vice Versa: seminar given by Enea Zaffanella at the Dipartimento di Informatica in Verona, Italy, on September 21st, 2004. Transparencies available in PostScript and PDF. A version of this seminar was given by Roberto Bagnara at the Dipartimento di Informatica, Sistemi e Produzione in Roma (Università degli Studi “Tor Vergata”), on November 29th, 2004. Transparencies available in PostScript and PDF.
Presentation of the paper Widening Operators for Weakly-Relational Numeric Abstractions given by Enea Zaffanella at the 12th International Symposium on Static Analysis (SAS’05 ), in London, UK, on September 8th, 2005. Transparencies available in PostScript and PDF.

Bibliographies

We have compiled a bibliography of articles and reports that we have used and/or written while developing the PPL.

We also have a bibliography of citations where we collect papers that cite our work in one form or another.

Licenses

The GNU General Public License, under which the library is distributed, is available in HTML, PDF, and PostScript.

The GNU Free Documentation License, under which the library documentation is distributed, is available in HTML, PDF, and PostScript.