path: root/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       [1] (University of Parma)
  Patricia M. Hill      [2] (University of Leeds)
  Enea Zaffanella       [3] (University of Parma)


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:
---------------------

  Abramo Bagnara        (Opera Unica) rewrote and generalized the
                        support for checked coefficients.  He also
                        wrote the support for extended numbers and is
                        currently writing a new implementation of
                        intervals.  He also helps on several other
                        design and implementation issues.

  Fabio Bossi           (student of the University of Parma)
                        is working on the PPL support for the approximation
                        of floating point computations.

  Francois Galea        [*] (University of Versailles) is working
                        at the implementation of the Parametric Integer
                        Programming solver.

  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.

  Enric Rodriguez Carbonell [4] (Technical University of Catalonia) is
                        working on the implementation of polynomial spaces.

  Alessandro Zaccagnini [5] (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       (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.

  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.

  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.

  Katy Dobson           [6] (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     (University of Parma) wrote the initial version
                        of the support for native and checked integer
                        coefficients.

  Maximiliano Marchesi  (former student of the University of Parma)
                        helped a little to improve the documentation for
                        bounded differences.

  Elena Mazzi           (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       [7] (formerly at the University of Leeds) worked
                        on the implementation of rational grids.  He has
                        also helped on other implementation issues.

  Andrea Pescetti       (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.

  Angela Stazzone       (former student of the University of Parma)
                        worked on the library's documentation.

  Fabio Trabucchi       (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.


  Frederic Besson       [8] provided useful comments and observations on
                        the ideas (about an extrapolation operator for
                        convex polyhedra) sketched in a paper he
                        coauthored in 1999.

  Tevfik Bultan         [9] (University of California, Santa Barbara)
                        suggested us to add support for generalized
                        affine transfer functions.  Discussions with
                        Tevfik have been very useful.

  Manuel Carro
  Jose Morales          [9, 10] members of the CLIP Group [12], helped us
                        to produce a Ciao Prolog [13] 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
                        Jose Manuel Gomez.

  Marco Comini          [14] (University of Udine) allows us to use his
                        Mac OS X machine to work on portability to
                        that platform.

  Goran Frehse          [15] (VERIMAG, formerly at Carnegie Mellon University)
                        provided very useful feedback while he was
                        developing PHAVer [16].  We are working with
                        Goran in order to include more polyhedra
                        simplification facilities in the PPL.

  Denis Gopan           [17] (University of Wisconsin-Madison) helped us
                        extend the library with the "expand space
                        dimension" and "fold space dimensions"
                        operations of the library.

  Martin Guy            [18] gave us access to his ARM machine: without
                        this possibility, porting the PPL to the ARM's
                        ABIs would have taken ages.

  Bruno Haible          [19] (ILOG) 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 in nonstandard places.

  Bertrand Jeannet      [20] (IRISA) wrote the New Polka library [21]
                        and made it available.  We had several
                        interesting exchanges with Bertrand concerning
                        various aspects of polyhedra manipulation.

  Herve Le Verge        (r.i.p.) wrote and published an implementation
                        [22] of the Chernikova's algorithm [23] that
                        has set the stage for subsequent
                        implementation work, including our own.

  Francesco Logozzo     [24] (formerly at Ecole Polytechnique) helped us
                        straighten out some portability issues on Cygwin.

  Kenneth MacKenzie     [25] provided very good bug reports that allowed
                        us to fix several problems in the OCaml interface.

  Costantino Medori     [26] (University of Parma) helped us on some
                        mathematical aspects of the development.

  Fred Mesnard          [27] (University of La Reunion), the main author
                        of cTI [28], 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 [29] 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.

  Ken Mixter            (then at Carnegie Mellon University) provided
                        useful feedback while working on an
                        experimental version of the Action Language
                        Verifier [30] based on the PPL.

  Sebastian Pop         [31] (now at AMD).  During his work on interfacing
                        CLooG [32] 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           [33] (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           [34] (Tel-Aviv University) stimulated the development
                        of the PPL by providing, in particular,
                        interesting challenges related to precision
                        and scalability.

  Sriram Sankaranarayanan [35] (NEC Laboratories America, formerly at
                        Stanford University) provided very useful feedback
                        while developing StInG [36] and LPInv [37].

  Axel Simon            [38] (ENS, formerly at the University of Kent
                        at Canterbury) wrote some PPL 0.9
                        bindings [44] for the Glasgow Haskell Compiler.

  Fausto Spoto          [39] (University of Verona) did useful beta testing
                        for the Java interface.  He also suggested the
                        addition of the <EM>hash code</EM> operations.

  Basile Starynkevitch  [40] (CEA LIST/DTSI/SOL). Basile is the author
                        of MELT [41] and suggested several improvements
                        to the PPL.


  Pedro Vasconcelos     [42] (formerly at the University of St Andrews, UK)
                        provided useful feedback while developing his
                        size and cost analyzer for Core Hume [43].
                        Pedro also solved a problem of Axel Simon's
                        PPL 0.9 bindings for the GHC and makes them
                        publicly available [44].

  Ralf Wildenhues       [45] (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 [46] has donated a bi-quad core machine with
  the latest AMD Opteron 2384 "Shanghai" processors and 16GB of RAM.
  This machine now hosts all the PPL data and services.  Many thanks
  to Christophe Harle and Sebastian Pop.

- The Computing Center of the University of Parma [47] allowed us to
  test the portability of the library on a variety of platforms.
  Fausto Pagani was especially helpful in this respect.

- The GCC Compile Farm Project [48] 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 [49]
  allowed us to complete the porting of the PPL to the IA64 and PA-RISC
  architectures.  Many thanks to Thibaut Varene [50] and the PA-RISC
  Linux community [51] for their kind assistance.

- HiPEAC [52] sponsored the participation of Roberto Bagnara to the
  Graphite Workshop [53].  This was very helpful to discuss the needs
  of Graphite [54] (a framework for high-level loop optimizations on
  the polyhedral model) and, more generally, of GCC [55] in terms of
  numerical abstractions and how the PPL can help.  Special thanks go
  to Albert Cohen [57] for this sponsorship.

- INRIA [56] is supporting 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 [57].


Some of our research work has been partly supported by the following
projects and organizations:

- University of Parma's FIL scientific research project (ex 60%)
  ``Pure and Applied Mathematics'';

- MURST project ``Automatic Program Certification by Abstract
  Interpretation'' [58];

- MURST project ``Abstract Interpretation, Type Systems and Control-Flow
  Analysis'';

- MURST project ``Automatic Aggregate- and Number-Reasoning for Computing:
  from Decision Algorithms to Constraint Programming with Multisets, Sets,
  and Maps'' [59];

- MURST project ``Constraint Based Verification of Reactive Systems'' [60];

- MURST project ``AIDA - Abstract Interpretation: Design and
  Applications'' [61];

- PRIN project ``AIDA 2007 - Abstract Interpretation: Design and
  Applications'' [62];

- Royal Society Joint project 2004/R1-EU (UK-Italy)
  ``Automatic Detection of Unstable Numerical Computations'';

- EPSRC (UK) project EP/C520726/1
  ``Numerical Domains for Software Analysis'' [63];

- Royal Society International Outgoing Short Visit 2007/R4
  ``Finding and Verifying the Absence of Bugs in Imperative Programs'' [64];

- EPSRC (UK) project EP/G025177/1
  ``Geometric Abstractions for Scalable Program Analyzers'' [64].

--------

 [1] http://www.cs.unipr.it/~bagnara/
 [2] http://www.comp.leeds.ac.uk/hill/
 [3] http://www.cs.unipr.it/~zaffanella/
 [*] http://www.prism.uvsq.fr/~fgalea/
 [4] http://www.lsi.upc.edu/~erodri/
 [5] http://www.math.unipr.it/~zaccagni/
 [6] http://www.comp.leeds.ac.uk/katyd/
 [7] http://www.mundell.ukfsn.org/
 [8] http://www.irisa.fr/lande/fbesson/fbesson.html
 [9] http://www.cs.ucsb.edu/~bultan/
[10] http://www.clip.dia.fi.upm.es/~boris/
[11] http://clip.dia.fi.upm.es/~jfran/
[12] http://clip.dia.fi.upm.es/
[13] http://clip.dia.fi.upm.es/Software/Ciao/
[14] http://www.dimi.uniud.it/~comini/
[15] http://www-verimag.imag.fr/~frehse/
[16] http://www-verimag.imag.fr/~frehse/phaver_web/
[17] http://www.cs.wisc.edu/~gopan/
[18] http://martinwguy.co.uk/
[19] http://www.haible.de/bruno/
[20] http://www.irisa.fr/prive/Bertrand.Jeannet/
[21] http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html
[22] http://www.cs.unipr.it/ppl/Documentation/chernikova.c
[23] http://www.cs.unipr.it/ppl/Documentation/bibliography#LeVerge92
[24] http://research.microsoft.com/~logozzo/
[25] http://homepages.inf.ed.ac.uk/kwxm/
[26] http://www.math.unipr.it/~medori/
[27] http://www.univ-reunion.fr/~fred/
[28] http://www.cs.unipr.it/cTI/
[29] http://www.cs.unipr.it/China/
[30] http://www.cs.ucsb.edu/~bultan/composite/
[31] http://www-rocq.inria.fr/~pop/
[32] http://www.cloog.org/
[33] http://www.cs.wisc.edu/~reps/
[34] http://www.math.tau.ac.il/~msagiv/
[35] http://www.nec-labs.com/~srirams/
[36] http://theory.stanford.edu/~srirams/Software/sting.html
[37] http://theory.stanford.edu/~srirams/Software/lpinv.html
[38] http://www.di.ens.fr/~simona/
[39] http://profs.sci.univr.it/~spoto/
[40] http://www.starynkevitch.net/Basile/index_en.html
[41] http://gcc.gnu.org/wiki/MiddleEndLispTranslator
[42] http://www.ncc.up.pt/~pbv/
[43] http://www.ncc.up.pt/~pbv/cgi/cost.cgi
[44] http://www.ncc.up.pt/~pbv/research/ppl/ghc.html
[45] http://wissrech.ins.uni-bonn.de/people/wildenhues.html
[46] http://developer.amd.com/
[47] http://www.siti.unipr.it/
[48] http://gcc.gnu.org/wiki/CompileFarm
[49] http://www.esiee.fr/
[50] http://www.parisc-linux.org/~varenet/
[51] http://www.parisc-linux.org/
[52] http://www.hipeac.net/
[53] http://gcc.gnu.org/wiki/Graphite_Workshop_Nov08
[54] http://gcc.gnu.org/wiki/Graphite
[55] http://gcc.gnu.org/
[56] http://www.inria.fr/
[57] http://www-rocq.inria.fr/~acohen/
[58] http://theory.sci.univr.it/p40/
[59] http://www.cs.unipr.it/Projects/COFIN01
[60] http://www.disi.unige.it/person/DelzannoG/cover/
[61] http://www.cs.unipr.it/Projects/AIDA/
[62] http://www.cs.unipr.it/Projects/AIDA2007/
[63] http://www.comp.leeds.ac.uk/hill/chiara/WWW/linda.html
[64] http://www.comp.leeds.ac.uk/hill/chiara/WWW/projects.html