
Authors
=======

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

  Roberto Bagnara [1]  <bagnara@cs.unipr.it>
  Patricia M. Hill [2] <hill@comp.leeds.ac.uk>
  Enea Zaffanella [3]  <zaffanella@cs.unipr.it>

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 <lucia.alessandrini@unipr.it> 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/
