Authors ======= The Parma Polyhedra Library and its documentation is being designed, written, debugged and improved by the following people: Roberto Bagnara [1] Patricia M. Hill [2] Enea Zaffanella [3] An important contributor to the development of the PPL, up until December 2002, was Elisa Ricci (former student of the University of Parma) The following people took part in the first phase of the library's development: Sara Bonini (former student of the University of Parma) Andrea Pescetti (University of Parma) Angela Stazzone (former student of the University of Parma) Tatiana Zolo (former student of the University of Parma) Thanks! ======= The following people have given help that has been fundamental to the project: + Herve' Le Verge (r.i.p.) wrote and published an implementation [4] of the Chernikova's algorithm [5] that has set the stage for subsequent implementation work, including our own. + Bertrand Jeannet [6] wrote the New Polka library [7] and made it available. + Lucia Alessandrini 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. + Costantino Medori [8] helped and continues to help us with mathematical aspects of the development. + Fred Mesnard [9], the main author of cTI [10], has given us access to a version of cTI's data-flow analyzer. The cTI system pioneered the concept of termination inference, a new kind of program analysis. When does a logic program terminate? cTI has been the _first_ system to answer this question with a compact formula, called termination condition. cTI's analyzer performs a linear size relation analysis using a domain of convex polyhedra. The China data-flow analyzer [11] uses the Parma Polyhedra Library to perform the same analysis. We run the two systems against each other, using them to analyze the same Prolog programs. Since the systems do not share a single line of code, this is giving us excellent opportunities for our testing and debugging work. + Alessandro Zaccagnini [12] is always a very valuable source of mathematical advice. + Bruno Haible [13] made it possible (by writing the AC_LIB_LINKFLAGS macro and explaining how to use it) to allow the use of versions of the GMP library installed into nonstandard places. This work has been partly supported by the following projects: 1. University of Parma's FIL scientific research project (ex 60%) ``Pure and Applied Mathematics''; 2. MURST project ``Automatic Program Certification by Abstract Interpretation'' [14]; 3. MURST project ``Abstract Interpretation, Type Systems and Control-Flow Analysis'' [15]. 4. MURST project ``Automatic Aggregate- and Number-Reasoning for Computing: from Decision Algorithms to Constraint Programming with Multisets, Sets, and Maps'' [16]. 5. MURST project ``Constraint Based Verification of Reactive Systems'' [17]. -------- [1] http://www.cs.unipr.it/~bagnara/ [2] http://www.comp.leeds.ac.uk/hill/ [3] http://www.cs.unipr.it/~zaffanella/ [4] http://www.cs.unipr.it/ppl/Documentation/chernikova.c [5] http://www.cs.unipr.it/ppl/Documentation/bibliography#LeVerge92 [6] http://www.irisa.fr/prive/Bertrand.Jeannet/ [7] http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html [8] http://www.math.unipr.it/~medori/ [9] http://www.univ-reunion.fr/~fred/ [10] http://www.cs.unipr.it/cTI/ [11] http://www.cs.unipr.it/China/ [12] http://www.math.unipr.it/~zaccagni/ [13] http://www.haible.de/bruno/ [14] http://theory.sci.univr.it/projects/p40/ [15] http://strudel.di.unipi.it/cofin00/ [16] http://www.cs.unipr.it/Projects/COFIN01 [17] http://www.disi.unige.it/person/DelzannoG/cover/