1 2Authors 3======= 4 5The Parma Polyhedra Library and its documentation is being designed, 6extended, written, debugged, maintained and improved by the following 7people: 8 9 10Core Development Team: 11---------------------- 12 13 Roberto Bagnara [1] (BUGSENG srl and University of Parma) 14 Patricia M. Hill [2] (BUGSENG srl and University of Leeds) 15 Abramo Bagnara (BUGSENG srl) 16 Enea Zaffanella [3] (University of Parma) 17 18 19Former Members of the Core Development Team: 20-------------------------------------------- 21 22 Elisa Ricci (former student of the University of Parma, 23 one of the four students with which the PPL 24 project started) has been a major contributor 25 to the development of the PPL, up until 26 December 2002. 27 28 29Current Contributors: 30--------------------- 31 32 Alessandro Zaccagnini [4] (University of Parma) has helped with 33 the efficient implementation of GCD and LCM 34 for checked numbers. He is now working on the 35 definitions of interval arithmetic operations. 36 Alessandro is always a very valuable source of 37 mathematical advice. 38 39 Paulo Cesar Pereira de Andrade 40 Helps with Fedora packaging. 41 42 43Past Contributors: 44------------------ 45 46 Roberto Amadini (former student of the University of Parma) 47 did some work on the PPL support for the 48 approximation of floating point computations. 49 50 Irene Bacchi (former student of the University of Parma) worked 51 on a development branch where she implemented 52 several variants of algorithms, checking 53 whether or not the set-union of two polyhedra 54 is the same as their poly-hull. 55 56 Massimo Benerecetti (University of Naples) worked on the positive 57 time-elapse operator on polyhedra. 58 59 Fabio Biselli (student of the University of Parma) 60 did some work on the PPL support for the 61 approximation of floating point computations. 62 63 Fabio Bossi (former student of the University of Parma) 64 worked on the PPL support for the approximation 65 of floating point computations. 66 67 Danilo Bonardi (former student of the University of Parma) worked 68 on a development branch where he experimented 69 with the use of metaprogramming techniques 70 based on expression templates. The objective 71 of this work was to check the effectiveness of 72 these techniques for moving computations from 73 run-time to compile-time. 74 75 Sara Bonini (former student of the University of Parma) is 76 one of the four students with which the PPL 77 project started. 78 79 Andrea Cimino (former student of the University of Parma) 80 wrote most of the mixed integer programming 81 solver, and also most of the Java and OCaml 82 interfaces. He helped us a lot with the web site. 83 84 Katy Dobson (former student of the University of Leeds) 85 worked on the formalization and definition of 86 algorithms for rational grids and products 87 of grids and polyhedra. 88 89 Marco Faella (University of Naples) worked on the positive 90 time-elapse operator on polyhedra. 91 92 Giordano Fracasso (former student of the University of Parma) wrote 93 the initial version of the support for native 94 and checked integer coefficients. 95 96 Francois Galea [5] (University of Versailles) worked 97 at the implementation of the Parametric Integer 98 Programming solver. 99 100 Maximiliano Marchesi (former student of the University of Parma) 101 helped a little to improve the documentation for 102 bounded differences. 103 104 Elena Mazzi (former student of the University of Parma) worked 105 on our implementation of bounded differences 106 and octagons. She also participated in the 107 theoretical and practical work concerning 108 widening operators for weakly relational 109 domains. 110 111 David Merchat (formerly at the University of Parma) helped us 112 with the generation of the library's documentation 113 using Doxygen. 114 115 Stefano Minopoli (University of Naples) worked on the positive 116 time-elapse operator on polyhedra. 117 118 Matthew Mundell [6] (formerly at the University of Leeds) worked 119 on the implementation of rational grids. He has 120 also helped on other implementation issues. 121 122 Andrea Pescetti (former student of the University of Parma) was one 123 of the four students with which the PPL 124 project started. Later, he helped a little 125 with the library's documentation. 126 127 Marco Poletti (former student of the University of Bologna) 128 implemented the sparse matrices that are used 129 in the MIP and PIP solvers of the PPL; he also 130 did experiments on the parallelization of the 131 sparse matrices' computations; he also worked 132 on improving the PPL's memory footprint and 133 on other improvements to the library. 134 135 Barbara Quartieri (former student of the University of Parma) worked 136 on our implementation of bounded differences and 137 octagons. 138 139 Enric Rodriguez Carbonell [7] (Technical University of Catalonia) 140 worked at the implementation of polynomial spaces. 141 142 Angela Stazzone (former student of the University of Parma) 143 worked on the library's documentation. 144 145 Fabio Trabucchi (former student of the University of Parma) worked 146 on a development branch where he added 147 serializers for all the objects of the PPL. 148 Support for serialization based on Fabio's 149 work will be available in a future release of 150 the library. 151 152 Claudio Trento (former student of the University of Pisa) did 153 a small amount of work on an experimental OCaml 154 interface for the PPL. 155 156 Tatiana Zolo (former student of the University of Parma) is 157 one of the four students with which the PPL 158 project started. 159 160 161 162Thanks! 163======= 164 165 166People: 167------- 168 169 Lucia Alessandrini (University of Parma) provided 4 hour-long 170 lectures on convex polyhedra for the Italian 171 authors. This was crucial for us to acquire 172 and/or refresh the notions needed for 173 developing the PPL library. 174 175 176 Frederic Besson [8] provided useful comments and observations on 177 the ideas (about an extrapolation operator for 178 convex polyhedra) sketched in a paper he 179 coauthored in 1999. 180 181 Tevfik Bultan [9] (University of California, Santa Barbara) 182 suggested us to add support for generalized 183 affine transfer functions. Discussions with 184 Tevfik have been very useful. 185 186 Manuel Carro 187 Jose Morales [9, 10] members of the CLIP Group [12], helped us 188 to produce a Ciao Prolog [13] interface for the 189 library. The decisive (and memorable) debugging 190 session took place in Parma in the afternoon of 191 March 10th, 2003, with the participation of 192 Jose Manuel Gomez. 193 194 Marco Comini [14] (University of Udine) allows us to use his 195 Mac OS X machine to work on portability to 196 that platform. 197 198 Goran Frehse [15] (VERIMAG, formerly at Carnegie Mellon University) 199 provided very useful feedback while he was 200 developing PHAVer [16]. We are working with 201 Goran in order to include more polyhedra 202 simplification facilities in the PPL. 203 204 Denis Gopan [17] (University of Wisconsin-Madison) helped us 205 extend the library with the "expand space 206 dimension" and "fold space dimensions" 207 operations of the library. 208 209 Martin Guy [18] gave us access to his ARM machine: without 210 this possibility, porting the PPL to the ARM's 211 ABIs would have taken ages. 212 213 Bruno Haible [19] (ILOG) helped us in our first steps towards 214 using versions of the GMP library installed in 215 nonstandard places. 216 217 Bertrand Jeannet [20] (IRISA) wrote the New Polka library [21] 218 and made it available. We had several 219 interesting exchanges with Bertrand concerning 220 various aspects of polyhedra manipulation. 221 222 Herve Le Verge (r.i.p.) wrote and published an implementation 223 [22] of the Chernikova's algorithm [23] that 224 has set the stage for subsequent 225 implementation work, including our own. 226 227 Francesco Logozzo [24] (formerly at Ecole Polytechnique) helped us 228 straighten out some portability issues on Cygwin. 229 230 Kenneth MacKenzie [25] provided very good bug reports that allowed 231 us to fix several problems in the OCaml interface. 232 233 Costantino Medori [26] (University of Parma) helped us on some 234 mathematical aspects of the development. 235 236 Fred Mesnard [27] (University of La Reunion), the main author 237 of cTI [28], has worked with us on one of the 238 first applications of the PPL: the "cTI" 239 data-flow analyzer, which performs a linear 240 size relation analysis using a domain of 241 convex polyhedra. The China data-flow 242 analyzer [29] uses the Parma Polyhedra Library 243 to perform the same analysis. We have been 244 running China against an old version of cTI 245 that did not use the PPL, using it to 246 analyze the same Prolog programs. Since these 247 systems did not share a single line of code, 248 this gave us excellent opportunities for our 249 initial testing and debugging work. Fred has 250 also helped us to port the PPL to Mac OS X. 251 252 Ken Mixter (then at Carnegie Mellon University) provided 253 useful feedback while working on an 254 experimental version of the Action Language 255 Verifier [30] based on the PPL. 256 257 Sebastian Pop [31] (now at AMD). During his work on interfacing 258 CLooG [32] with the PPL, Sebastian provided 259 valuable feedback, particularly on the C 260 interface to the PPL. He also suggested the 261 addition of new functionality such as the 262 "simplify using context" operation. 263 264 Thomas Reps [33] (University of Wisconsin-Madison), on several 265 occasions we have had interesting discussions 266 with him both on the PPL and on the more 267 general topics of static analysis and 268 numerical abstractions. 269 270 Mooly Sagiv [34] (Tel-Aviv University) stimulated the development 271 of the PPL by providing, in particular, 272 interesting challenges related to precision 273 and scalability. 274 275 Sriram Sankaranarayanan [35] (NEC Laboratories America, formerly at 276 Stanford University) provided very useful feedback 277 while developing StInG [36] and LPInv [37]. 278 279 Axel Simon [38] (ENS, formerly at the University of Kent 280 at Canterbury) wrote some PPL 0.9 281 bindings [44] for the Glasgow Haskell Compiler. 282 283 Fausto Spoto [39] (University of Verona) did useful beta testing 284 for the Java interface. He also suggested the 285 addition of the <EM>hash code</EM> operations. 286 287 Basile Starynkevitch [40] (CEA LIST/DTSI/SOL). Basile is the author 288 of MELT [41] and suggested several improvements 289 to the PPL. 290 291 292 Pedro Vasconcelos [42] (formerly at the University of St Andrews, UK) 293 provided useful feedback while developing his 294 size and cost analyzer for Core Hume [43]. 295 Pedro also solved a problem of Axel Simon's 296 PPL 0.9 bindings for the GHC and makes them 297 publicly available [44]. 298 299 Ralf Wildenhues [45] (University of Bonn) helped us with 300 several issues concerning the proper use of 301 the Autotools. 302 303 304Organizations (and People Therein): 305----------------------------------- 306 307We are grateful for the following contributions: 308 309- AMD Developer Central [46] has donated a bi-quad core machine with 310 the latest AMD Opteron 2384 "Shanghai" processors and 16GB of RAM. 311 This machine now hosts all the PPL data and services. Many thanks 312 to Christophe Harle and Sebastian Pop. 313 314- The Computing Center of the University of Parma [47] allowed us to 315 test the portability of the library on a variety of platforms. 316 Fausto Pagani was especially helpful in this respect. 317 318- The GCC Compile Farm Project [48] managed by FSF France provided 319 access to a number of machines that allowed us to test and improve 320 the portability of the library. Special thanks go to Laurent Guerby 321 for his kind assistance. 322 323- The test cluster provided by Hewlett Packard and hosted by ESIEE [49] 324 allowed us to complete the porting of the PPL to the IA64 and PA-RISC 325 architectures. Many thanks to Thibaut Varene [50] and the PA-RISC 326 Linux community [51] for their kind assistance. 327 328- HiPEAC [52] sponsored the participation of Roberto Bagnara to the 329 Graphite Workshop [53]. This was very helpful to discuss the needs 330 of Graphite [54] (a framework for high-level loop optimizations on 331 the polyhedral model) and, more generally, of GCC [55] in terms of 332 numerical abstractions and how the PPL can help. Special thanks go 333 to Albert Cohen [57] for this sponsorship. 334 335- INRIA [56] supported the work of Abramo Bagnara from January 1st to 336 May 31st, 2009, to work on the PPL and its development 337 infrastructure. Many thanks go, in particular, to Albert Cohen [57]. 338 339 340Some of our research work has been partly supported by the following 341projects and organizations: 342 343- University of Parma's FIL scientific research project (ex 60%) 344 ``Pure and Applied Mathematics''; 345 346- MURST project ``Automatic Program Certification by Abstract 347 Interpretation'' [58]; 348 349- MURST project ``Abstract Interpretation, Type Systems and Control-Flow 350 Analysis''; 351 352- MURST project ``Automatic Aggregate- and Number-Reasoning for Computing: 353 from Decision Algorithms to Constraint Programming with Multisets, Sets, 354 and Maps'' [59]; 355 356- MURST project ``Constraint Based Verification of Reactive Systems'' [60]; 357 358- MURST project ``AIDA - Abstract Interpretation: Design and 359 Applications'' [61]; 360 361- PRIN project ``AIDA 2007 - Abstract Interpretation: Design and 362 Applications'' [62]; 363 364- Integrated Action Italy-Spain 2001-2002 ``Advanced Development Environments 365 for Logic Programs'' [63]; 366 367- Royal Society Joint project 2004/R1-EU (UK-Italy) 368 ``Automatic Detection of Unstable Numerical Computations''; 369 370- EPSRC (UK) project EP/C520726/1 371 ``Numerical Domains for Software Analysis'' [64]; 372 373- Royal Society International Outgoing Short Visit 2007/R4 374 ``Finding and Verifying the Absence of Bugs in Imperative Programs'' [65]; 375 376- EPSRC (UK) project EP/G025177/1 377 ``Geometric Abstractions for Scalable Program Analyzers'' [65]. 378 379-------- 380 381 [1] http://www.cs.unipr.it/~bagnara/ 382 [2] http://www.comp.leeds.ac.uk/hill/ 383 [3] http://www.cs.unipr.it/~zaffanella/ 384 [4] http://www.math.unipr.it/~zaccagni/ 385 [5] http://fgalea.free.fr/ 386 [6] http://www.mundell.ukfsn.org/ 387 [7] http://www.lsi.upc.edu/~erodri/ 388 [8] http://www.irisa.fr/lande/fbesson/fbesson.html 389 [9] http://www.cs.ucsb.edu/~bultan/ 390[10] http://www.clip.dia.fi.upm.es/~boris/ 391[11] http://clip.dia.fi.upm.es/~jfran/ 392[12] http://clip.dia.fi.upm.es/ 393[13] http://clip.dia.fi.upm.es/Software/Ciao/ 394[14] http://www.dimi.uniud.it/~comini/ 395[15] http://www-verimag.imag.fr/~frehse/ 396[16] http://www-verimag.imag.fr/~frehse/phaver_web/ 397[17] http://www.cs.wisc.edu/~gopan/ 398[18] http://martinwguy.co.uk/ 399[19] http://www.haible.de/bruno/ 400[20] http://www.irisa.fr/prive/Bertrand.Jeannet/ 401[21] http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html 402[22] http://bugseng.com/products/ppl/documentation/chernikova.c 403[23] http://bugseng.com/products/ppl/documentation/bibliography#LeVerge92 404[24] http://research.microsoft.com/~logozzo/ 405[25] http://homepages.inf.ed.ac.uk/kwxm/ 406[26] http://www.math.unipr.it/~medori/ 407[27] http://www.univ-reunion.fr/~fred/ 408[28] http://www.cs.unipr.it/cTI/ 409[29] http://www.cs.unipr.it/China/ 410[30] http://www.cs.ucsb.edu/~bultan/composite/ 411[31] http://www-rocq.inria.fr/~pop/ 412[32] http://www.cloog.org/ 413[33] http://www.cs.wisc.edu/~reps/ 414[34] http://www.math.tau.ac.il/~msagiv/ 415[35] http://www.nec-labs.com/~srirams/ 416[36] http://theory.stanford.edu/~srirams/Software/sting.html 417[37] http://theory.stanford.edu/~srirams/Software/lpinv.html 418[38] http://www.di.ens.fr/~simona/ 419[39] http://profs.sci.univr.it/~spoto/ 420[40] http://www.starynkevitch.net/Basile/index_en.html 421[41] http://gcc.gnu.org/wiki/MiddleEndLispTranslator 422[42] http://www.ncc.up.pt/~pbv/ 423[43] http://www.ncc.up.pt/~pbv/cgi/cost.cgi 424[44] http://www.ncc.up.pt/~pbv/research/ppl/ghc.html 425[45] http://wissrech.ins.uni-bonn.de/people/wildenhues.html 426[46] http://developer.amd.com/ 427[47] http://www.siti.unipr.it/ 428[48] http://gcc.gnu.org/wiki/CompileFarm 429[49] http://www.esiee.fr/ 430[50] http://www.parisc-linux.org/~varenet/ 431[51] http://www.parisc-linux.org/ 432[52] http://www.hipeac.net/ 433[53] http://gcc.gnu.org/wiki/Graphite_Workshop_Nov08 434[54] http://gcc.gnu.org/wiki/Graphite 435[55] http://gcc.gnu.org/ 436[56] http://www.inria.fr/ 437[57] http://www-rocq.inria.fr/~acohen/ 438[58] http://theory.sci.univr.it/p40/ 439[59] http://www.cs.unipr.it/Projects/COFIN01 440[60] http://www.disi.unige.it/person/DelzannoG/cover/ 441[61] http://www.cs.unipr.it/Projects/AIDA/ 442[62] http://www.cs.unipr.it/Projects/AIDA2007/ 443[63] http://www.cs.unipr.it/Projects/AzInt2001-2002Sp 444[64] http://www.comp.leeds.ac.uk/hill/chiara/WWW/linda.html 445[65] http://www.comp.leeds.ac.uk/hill/chiara/WWW/projects.html 446