This page is devoted to the applications and projects that rely on the Parma Polyhedra Library. Here are the ones we are aware of.
- Jandom, an abstract interpretation based static analyzer written in Scala.
- RTSCAN (Real-Time-SC-hedulability -AN-alyser), a set of libraries and programs for performing scheduling analysis of real-time systems.
- The Sage mathematics software system uses the Parma Polyhedra Library for polyhedral computations. This includes a Python/Cython interface on which Sage's polyhedral objects are based.
- The SpaceEx tool platform facilitates the implementation of algorithms related to reachability and safety verification.
- Graphite (Gimple Represented as Polyhedra), a framework for high-level loop optimizations that is now part of GCC (the GNU Compiler Collection), uses the Parma Polyhedra Library.
- IMITATOR (Inverse Method for Inferring Time AbstracT behaviOR) performs constraint synthesis on parametric timed automata.
- Julia: a generic static analyser for full sequential Java bytecode. Julia is written in Java and accesses the PPL via its Java interface.
- Fortuna is a model checker for priced probabilistic timed automata. It heavily uses the Parma Polyhedra Library.
- MELT (Middle End Lisp Translator), an experimental branch of GCC (the GNU Compiler Collection), will use the Parma Polyhedra Library for global static analysis.
- BIOCHAM: the Biochemical Abstract Machine.
- Pedro Vasconcelos wrote a size and cost analyzer for Core Hume that uses the PPL.
- Roméo, a tool for Time Petri Nets analysis.
- GENEPI, a GENEric Presburger programming Interface.
- The CHINA data-flow analyzer uses the library to detect linear size-relations among argument positions and to approximate the success-set of CLP programs.
- cTI, the first bottom-up left-termination inference tool for ISO-Prolog, also uses the PPL library for detecting linear size-relations among argument positions. These are then used to produce termination conditions for the analyzed program.
- Henning Meyer has developed a program to compute various aspects of tropical polytopes.
- Ron Ellenbogen has written, under the joint supervision of Nurit Dor, Mooly Sagiv, and Roberto Bagnara a version of CSSV (C String Static Verifier) based on the PPL.
- An experimental version, based on the PPL, of the Action Language Verifier has been produced by Ken Mixter (then at Carnegie Mellon University), under the direction of Tevfik Bultan.
- The Polyhedral Hybrid Automation Verifier (PHAVer) is a tool for verifying safety properties of Linear Hybrid Automata using the polyhedral computations offered by the PPL, written by Goran Frehse (then at the Department of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, USA). PHAVer exploits the ability of the PPL to represent finite disjunctions of convex polyhedra, so as to allow for non-convex polyhedral approximations. Goran reports that his tool compares favorably with HyTech and that he is quite pleased with the speed of the PPL.
- A version of TVLA, a system for shape analysis, that uses the PPL to reason about numeric properties has been developed by Denis Gopan, Computer Science Department, University of Wisconsin, Madison, USA.
- The Stanford Invariant Generator (StInG), based on the research work of Sriram Sankaranarayanan, Michael Colon, Henny Sipma and Zohar Manna, automatically computes linear invariants for linear transition systems using the PPL. Among other things, it exercises our BHRZ03 widening operator (see [BHRZ03]).
- The Linear Programming Invariant Generator (LPInv), based on the research work of Sriram Sankaranarayanan, Henny Sipma and Zohar Manna, computes linear invariants using a Linear Programming solver and then uses the PPL to perform a reliable correctness check for the computed invariants.
- François Gobert, Gustavo Ospina, and Baudouin Le Charlier wrote a static analyser of Prolog programs: it is written in Java and accesses the PPL via its C interface
- Ariadne: An open tool for hybrid system analysis.
- CHA: Convex Hull Analyser for logic programs.
These and other applications are described in papers listed in the bibliography of citations. Any help to keep this page and the bibliography up-to-date will be greatly appreciated.