-
Notifications
You must be signed in to change notification settings - Fork 0
/
CREDITS
445 lines (349 loc) · 19.6 KB
/
CREDITS
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
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] (BUGSENG srl and University of Parma)
Patricia M. Hill [2] (BUGSENG srl and University of Leeds)
Abramo Bagnara (BUGSENG srl)
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:
---------------------
Alessandro Zaccagnini [4] (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.
Paulo Cesar Pereira de Andrade
Helps with Fedora packaging.
Past Contributors:
------------------
Roberto Amadini (former 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.
Massimo Benerecetti (University of Naples) worked on the positive
time-elapse operator on polyhedra.
Fabio Biselli (student of the University of Parma)
did some work on the PPL support for the
approximation of floating point computations.
Fabio Bossi (former student of the University of Parma)
worked 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. He helped us a lot with the web site.
Katy Dobson (former student of the University of Leeds)
worked on the formalization and definition of
algorithms for rational grids and products
of grids and polyhedra.
Marco Faella (University of Naples) worked on the positive
time-elapse operator on polyhedra.
Giordano Fracasso (former student of the University of Parma) wrote
the initial version of the support for native
and checked integer coefficients.
Francois Galea [5] (University of Versailles) worked
at the implementation of the Parametric Integer
Programming solver.
Maximiliano Marchesi (former student of the University of Parma)
helped a little to improve the documentation for
bounded differences.
Elena Mazzi (former student of the 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.
Stefano Minopoli (University of Naples) worked on the positive
time-elapse operator on polyhedra.
Matthew Mundell [6] (formerly at the University of Leeds) worked
on the implementation of rational grids. He has
also helped on other implementation issues.
Andrea Pescetti (former student of the 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.
Marco Poletti (former 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 also worked
on improving the PPL's memory footprint and
on other improvements to the library.
Barbara Quartieri (former student of the University of Parma) worked
on our implementation of bounded differences and
octagons.
Enric Rodriguez Carbonell [7] (Technical University of Catalonia)
worked at the implementation of polynomial spaces.
Angela Stazzone (former student of the University of Parma)
worked on the library's documentation.
Fabio Trabucchi (former student of the 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) helped us in our first steps towards
using 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. Fred has
also helped us to port the PPL to Mac OS X.
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] supported the work of 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];
- Integrated Action Italy-Spain 2001-2002 ``Advanced Development Environments
for Logic Programs'' [63];
- 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'' [64];
- Royal Society International Outgoing Short Visit 2007/R4
``Finding and Verifying the Absence of Bugs in Imperative Programs'' [65];
- EPSRC (UK) project EP/G025177/1
``Geometric Abstractions for Scalable Program Analyzers'' [65].
--------
[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.math.unipr.it/~zaccagni/
[5] http://fgalea.free.fr/
[6] http://www.mundell.ukfsn.org/
[7] http://www.lsi.upc.edu/~erodri/
[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://bugseng.com/products/ppl/documentation/chernikova.c
[23] http://bugseng.com/products/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.cs.unipr.it/Projects/AzInt2001-2002Sp
[64] http://www.comp.leeds.ac.uk/hill/chiara/WWW/linda.html
[65] http://www.comp.leeds.ac.uk/hill/chiara/WWW/projects.html