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 hash code 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