PPL Credits

Authors

The Parma Polyhedra Library and its documentation is being designed, extended, written, debugged, maintained and improved by the following people:

Core Development Team

Roberto Bagnara (BUGSENG srl and University of Parma)
Patricia M. Hill (BUGSENG srl and University of Leeds)
Enea Zaffanella (University of Parma)
Abramo Bagnara (BUGSENG srl)

Former Members of the Core Development Team

Elisa Ricci (former student of the University of Parma, one of the four students with which the PPL project started) has been a major contributor to the development of the PPL, up until December 2002.

Current Contributors

Andrea Cimino (former student of the University of Parma) wrote most of the mixed integer programming solver, and also most of the Java and OCaml interfaces. He keeps helping us, especially with the web site.
Marco Poletti (student of the University of Bologna) implemented the sparse matrices that are used in the MIP and PIP solvers of the PPL; he also did experiments on the parallelization of the sparse matrices' computations; he is now working on improving the PPL's memory footprint and on other improvements to the library.
Alessandro Zaccagnini (University of Parma) has helped with the efficient implementation of GCD and LCM for checked numbers. He is now working on the definitions of interval arithmetic operations. Alessandro is always a very valuable source of mathematical advice.

Past Contributors

Roberto Amadini (former student of the University of Parma) did some work on the PPL support for the approximation of floating point computations.
Irene Bacchi (former student of the University of Parma) worked on a development branch where she implemented several variants of algorithms, checking whether or not the set-union of two polyhedra is the same as their poly-hull.
Fabio Biselli (student of the University of Parma) did some work on the PPL support for the approximation of floating point computations.
Fabio Bossi (former student of the University of Parma) worked on the PPL support for the approximation of floating point computations.
Danilo Bonardi (former student of the University of Parma) worked on a development branch where he experimented with the use of metaprogramming techniques based on expression templates. The objective of this work was to check the effectiveness of these techniques for moving computations from run-time to compile-time.
Sara Bonini (former student of the University of Parma) is one of the four students with which the PPL project started.
Katy Dobson (former student of the University of Leeds) worked on the formalization and definition of algorithms for rational grids and products of grids and polyhedra.
Giordano Fracasso (former student of the University of Parma) wrote the initial version of the support for native and checked integer coefficients.
François Galea (University of Versailles) worked at the implementation of the Parametric Integer Programming solver.
Maximiliano Marchesi (former student of the University of Parma) helped a little to improve the documentation for bounded differences.
Elena Mazzi (former student of the University of Parma) worked on our implementation of bounded differences and octagons. She also participated in the theoretical and practical work concerning widening operators for weakly relational domains.
David Merchat (formerly at the University of Parma) helped us with the generation of the library's documentation using Doxygen.
Matthew Mundell (formerly at the University of Leeds) worked on the implementation of rational grids. He has also helped on other implementation issues.
Andrea Pescetti (former student of the University of Parma) was one of the four students with which the PPL project started. Later, he helped a little with the library's documentation.
Barbara Quartieri (former student of the University of Parma) worked on our implementation of bounded differences and octagons.
Enric Rodríguez Carbonell worked on the implementation of polynomial spaces.
Angela Stazzone (former student of the University of Parma) worked on the library's documentation.
Fabio Trabucchi (former student of the University of Parma) worked on a development branch where he added serializers for all the objects of the PPL. Support for serialization based on Fabio's work, will be available in a future release of the library.
Claudio Trento (former student of the University of Pisa) did a small amount of work on an experimental OCaml interface for the PPL.
Tatiana Zolo (former student of the University of Parma) is one of the four students with which the PPL project started.

Thanks!

People

Lucia Alessandrini (University of Parma) provided 4 hour-long lectures on convex polyhedra for the Italian authors. This was crucial for us to acquire and/or refresh the notions needed for developing the PPL library.
Frédéric Besson provided useful comments and observations on the ideas sketched in [BJT99] .
Tevfik Bultan (University of California, Santa Barbara) suggested to us to add support for generalized affine transfer functions. Discussions with Tevfik have been very useful.
Manuel Carro and José Morales, members of the CLIP Group, helped us to produce a Ciao Prolog interface for the library. The decisive (and memorable) debugging session took place in Parma in the afternoon of March 10th, 2003, with the participation of José Manuel Gómez.
Marco Comini (University of Udine) allows us to use his Mac OS X machine to work on portability to that platform.
Goran Frehse (VERIMAG, formerly at Carnegie Mellon University) provided very useful feedback while he was developing PHAVer. We are working with Goran in order to include more polyhedra simplification facilities in the PPL.
Denis Gopan, (University of Wisconsin-Madison) a coauthor of [GDD + 04] , has helped us extend the library with the expand space dimension and fold space dimensions operations of the library.
Martin Guy gave us access to his ARM machine: without this possibility, porting the PPL to the ARM's ABIs would have taken ages.
Bruno Haible (ILOG) helped us in our first steps towards using versions of the GMP library installed in nonstandard places.
Bertrand Jeannet (IRISA) wrote the New Polka library and made it available. We had several interesting exchanges with Bertrand concerning various aspects of polyhedra manipulation.
Hervé Le Verge (r.i.p.) wrote and published an implementation of the [Chernikova's algorithm] that has set the stage for subsequent implementation work, including our own.
Francesco Logozzo (formerly at Ecole Polytechnique) helped us straighten out some portability issues on Cygwin
Kenneth MacKenzie provided very good bug reports that allowed us to fix several problems in the OCaml interface.
Costantino Medori helped us on some mathematical aspects of the development.
Fred Mesnard, the main author of cTI, has worked with us on one of the first applications of the PPL: the "cTI" data-flow analyzer, which performs a linear size relation analysis using a domain of convex polyhedra. The China data-flow analyzer uses the Parma Polyhedra Library to perform the same analysis. We have been running China against an old version of cTI that did not use the PPL, using it to analyze the same Prolog programs. Since these systems did not share a single line of code, this gave us excellent opportunities for our initial testing and debugging work. Fred has also helped us to port the PPL to Mac OS X.
Ken Mixter (then at Carnegie Mellon University) provided useful feedback while working on an experimental version of the Action Language Verifier based on the PPL.
Sebastian Pop (now at AMD). During his work on interfacing CLooG with the PPL, Sebastian provided valuable feedback, particularly on the C interface to the PPL. He also suggested the addition of new functionality such as the simplify using context operation.
Thomas Reps (University of Wisconsin-Madison) , on several occasions we have had interesting discussions with him both on the PPL and on the more general topics of static analysis and numerical abstractions.
Mooly Sagiv stimulated the development of the PPL by providing, in particular, interesting challenges related to precision and scalability.
Sriram Sankaranarayanan (NEC Laboratories America, formerly at Stanford University) provided very useful feedback while developing StInG and LPInv.
Axel Simon (ENS, formerly at the University of Kent at Canterbury) wrote some PPL 0.9 bindings for the Glasgow Haskell Compiler (GHC).
Fausto Spoto did useful beta testing for the Java interface. He also suggested the addition of the hash code operations.
Basile Starynkevitch (CEA LIST/DTSI/SOL). Basile is the author of MELT and suggested several improvements to the PPL.
Pedro Vasconcelos (formerly at the University of St Andrews, UK) provided useful feedback while developing his size and cost analyzer for Core Hume. Pedro also solved a problem of Axel Simon's PPL 0.9 bindings for the GHC and makes them publicly available.
Ralf Wildenhues (University of Bonn) helped us with several issues concerning the proper use of the Autotools.

Organizations (and People Therein)

We are grateful for the following contributions:

AMD Developer Central has donated a bi-quad core machine with the latest AMD Opteron 2384 "Shanghai" processors and 16GB of RAM. This machine is extensively used for regression-testing of the PPL. Many thanks to Christophe Harle and Sebastian Pop.
The Computing Center of the University of Parma allowed us to test the [portability] of the library on a variety of platforms. Fausto Pagani has been especially helpful in this respect.
The GCC Compile Farm Project managed by FSF France provided access to a number of machines that allowed us to test and improve the portability of the library. Special thanks go to Laurent Guerby for his kind assistance.
The test cluster provided by Hewlett Packard and hosted by ESIEE allowed us to complete the porting of the PPL to the IA64 and PA-RISC architectures. Many thanks to Thibaut Varène and the PA-RISC Linux community for their kind assistance.
HiPEAC sponsored the participation of Roberto Bagnara to the Graphite Workshop. This was very helpful to discuss the needs of Graphite (a framework for high-level loop optimizations on the polyhedral model) and, more generally, of GCC in terms of numerical abstractions and how the PPL can help. Special thanks go to Albert Cohen for this sponsorship.
INRIA supported the work Abramo Bagnara from January 1st to May 31st, 2009, to work on the PPL and its development infrastructure. Many thanks go, in particular, to Albert Cohen.

History

Here is, more or less, the history of the Parma Polyhedra Library.

The Beginning

The Parma Polyhedra Library began as the project of an advanced programming techniques course, Programmazione (Metodi Avanzati), taught by Roberto Bagnara with the help of Enea Zaffanella at the Department of Mathematics of the University of Parma, Italy.

The course ran from October 2000 to mid June 2001, and was taken by a select group of good (undergraduate) students: Sara Bonini, Andrea Pescetti, Elisa Ricci, and Tatiana Zolo.

The course project that has become known as the Parma Polyhedra Library project was chosen for the following reasons:

the teachers needed a powerful C++ convex polyhedra library for use in the China project and other research projects they are involved in;
all the students were about to graduate in Mathematics, so they were not scared of seemingly misspelled terms like lineality space;
moreover, in case of any trouble, we had a good security net: the Department of Mathematics, where we had no difficulty in obtaining expert advice (see the [credits page] for more on this);
people like Hervé Le Verge, Doran Wilde, Bertrand Jeannet, Komei Fukuda and others have published code and information that provided something to start and experiment with (more on the [credits] and the [links] pages).

Angela

For three months, starting from April 2001, Angela Stazzone had a consultancy contract to work full-time on the library. She worked on the documentation of the library.

Pat Joins the Team

Since the beginning of June 2001 Patricia M. Hill joined the effort and has been, since then, part of the stable development team.

Elisa

On September 2001, Elisa Ricci started working on her dissertation for the laurea degree in Mathematica. The dissertation, which is focused on the theoretical aspects of double descriptions and of the algorithms that operate upon them, was brilliantly defended on July 23, 2002.

For three months, starting from September 2002, Elisa had a consultancy contract to work full-time on the library. During that period she, among other things, extended the PPL testsuite so as to cover 100% of the library's code.

Elena and Barbara

The 2002-2003 edition of the course Programmazione (Metodi Avanzati), again taught by Roberto Bagnara with the help of Enea Zaffanella, was followed, among others, by Elena Mazzi and Barbara Quartieri.

The course ran from October 2002 to mid June 2003. Starting from May 2003, Elena and Barbara started their project on extending the PPL with an implementation of bounded differences and simple sections/octagons. They developed prototype implementations that now form the basis of the BD_Shape class that was included in version 0.9 and the Octagonal_Shape class included in version 0.10.

Maximiliano

A course on writing for mathematics and computer science, Scrittura Matematica e Informatica, taught in the second semester of academic year 2003-2004 by Roberto Bagnara with the help of Alessandro Zaccagnini at the Department of Mathematics of the University of Parma, was followed, among others, by Maximiliano Marchesi. Maximiliano did a course project in which he worked at the PPL documentation.

Gang of Five

Another course on programming techniques, Metodologie di Programmazione, taught by Enea Zaffanella with the help of Roberto Bagnara for the students of the first-level degree in Computer Science at the University of Parma, ran from October 2003 to January 2004. Several small/medium sized programming projects were assigned that are related to the development of the PPL. In particular:

Irene Bacchi worked on an implementation of the algorithms proposed in the paper Convexity Recognition of the Union of Polyhedra by Alberto Bemporad, Komei Fukuda, and Fabio Torrisi;
Danilo Bonardi worked on so-called expression templates for the optimization of the allocation of temporaries;
Andrea Cimino worked on an implementation of the simplex algorithm based on integer arithmetic;
Giordano Fracasso worked on alternative coefficient implementations, including native integer types with overflow detection;
Fabio Trabucchi worked on serialization and deserialization operators for the objects manipulated by the PPL.

The contribution of Andrea Cimino is part of the PPL since version 0.8. The contribution of Giordano Fracasso has been superseded by the work of Abramo Bagnara (see below). All of the other contributions, when suitably engineered and integrated in the main development line, will appear in future releases of the library.

Katy

After investigating previous work on a domain called Z-polyhedra [Anc91], Patricia Hill began a project aimed at the development of a domain of grids, a generalization of the well-known lattice domain.

In October 2003, Katy Dobson started work as a research student at the University of Leeds under the supervision of Patricia Hill to work on the representation of the Grid Domain and algorithms needed for the main operators on this domain.

More recently, Katy has studied reduction algorithms needed for the product of the grids with other polyhedral domains, including the octagonal shape and bounded difference shape domains. It is expected that some of these will be implemented and included in future releases of the library.

OCaml Interface

Claudio Trento, a student of the first-level degree in Computer Science of the University of Pisa, decided to devote the final project of his course of studies to an OCaml interface for the PPL. He obtained a preliminary, very rough interface and then vanished. His work has been superseded by the work of Andrea Cimino (see below).

Abramo Joins the Team

At the end of June 2004, Abramo Bagnara, an independent consultant and software professional, began a short contract, engineering some experimental features of the PPL. His first task was to provide a robust and general implementation of checked native integer arithmetic, which first appeared in PPL 0.7. He then started drafting a brand new and wholly generic implementation of intervals. This appears, in draft form, in PPL 0.10. Abramo is part now part of the core development team.

Matthew

Matthew Mundell joined the group in Leeds for 14 months in 2005-2006 and implemented the domain of grids that was included in the 0.9 release of the PPL. Matthew also helped in improving the design of the PPL testsuite and initiated work on a product domain which has subsequently been developed into the templatic partially reduced product domain that is included in PPL 0.10.

Andrea Strikes Back

From July to November 2006, Andrea Cimino has done contract work on the refinement of the PPL mixed integer linear programming solver and on the development of the Java and OCaml interfaces of the libraries. The latter were first released as part of PPL 0.10. Andrea, who continues to work with us in his spare time as an unpaid volunteer, also developed an experimental interface between the PPL and GLPK, the GNU linear programming kit.

Graphite

On Sunday, August 3, 2008, the core development team was enjoying summer when Sebastian Pop sent this message. At that time we came from a period where we had been working full-time on a program analyzer and, while we knew that we would have released PPL 0.10 one day, this was not yet scheduled. We thus changed our priorities and said that we [expected] the release to occur in a month or so. In reality, the release took three full months of hard work: this was the punishment for not having followed the first part of the motto

Release early. Release often. And listen to your customers.

But hey, concerning the second part of the motto, we believe no one can complain!

To Be Continued

...