This page is devoted to the applications and
projects that rely on the Parma Polyhedra Library.
Here are the ones we are aware of.
-
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.
