Imported Upstream version 0.11.2upstream/0.11.2upstream

1 files changed, 433 insertions, 0 deletions

diff --git a/CREDITS b/CREDITS
new file mode 100644
index 000000000..c88eca7ef
--- /dev/null
+++ b/CREDITS
@@ -0,0 +1,433 @@
+
+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