1: % Upper-case    A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

2: % Lower-case    a b c d e f g h i j k l m n o p q r s t u v w x y z

3: % Digits        0 1 2 3 4 5 6 7 8 9

4: % Exclamation   !           Double quote "          Hash (number) #

5: % Dollar        $           Percent      %          Ampersand     &

6: % Acute accent  '           Left paren   (          Right paren   )

7: % Asterisk      *           Plus         +          Comma         ,

8: % Minus         -           Point        .          Solidus       /

9: % Colon         :           Semicolon    ;          Less than     <

10: % Equals        =           Greater than >          Question mark ?

11: % At            @           Left bracket [          Backslash     \

12: % Right bracket ]           Circumflex   ^          Underscore    _

13: % Grave accent  `           Left brace   {          Vertical bar  |

14: % Right brace   }           Tilde

15: 

16: \documentclass[final]{elsart}

17: 

18: \journal{Science of Computer Programming}

19: \date{}

20: 

21: % Trick to circumvent a conflict between elsart and amsmath.

22: % Suggested by Simon Pepping <S.PEPPING@elsevier.nl>

23: % on Monday, 13 May 1996.

24: \mathchardef\Omega="700A

25: 

26: \usepackage{amsmath}

27: \usepackage{amssymb}

28: \usepackage{stmaryrd}

29: \usepackage{url}

30: \usepackage{verbatim}

31: \usepackage{ifthen}

32: \usepackage{varioref}

33: \usepackage{hhline}

34: \usepackage{dcolumn}

35: \usepackage{longtable}

36: \usepackage{pstricks,pst-node,pst-plot}

37: 

38: % Babel.

39: \usepackage[italian,english]{babel}

40: \newcommand{\english}[1]{\foreignlanguage{english}{#1}}

41: \newcommand{\italian}[1]{\foreignlanguage{italian}{#1}}

42: 

43: % Listings.

44: \usepackage{listings}

45: \lstloadlanguages{[ISO]C++,Prolog}

46: 

47: %% Table entries aligned on the decimal point.

48: \newcolumntype{.}{D{.}{.}{-1}}

49: 

50: %% C++

51: \newcommand*{\Cplusplus}{{C\nolinebreak[4]\hspace{-.05em}\raisebox{.4ex}{\tiny\bf ++}}}

52: 

53: %% Logical quantifiers stuff

54: \newcommand{\st}{\mathrel{.}}

55: \newcommand{\itc}{\mathrel{:}}

56: 

57: %% Special letters denoting sets and algebras

58: \providecommand*{\Nset}{\mathbb{N}}            % Naturals

59: \providecommand*{\Zset}{\mathbb{Z}}            % Integers

60: \providecommand*{\Qset}{\mathbb{Q}}            % Rationals

61: \providecommand*{\nonnegQset}{\mathbb{Q}_{\scriptscriptstyle{+}}}

62:                                                % Non-negative rationals

63: \providecommand*{\Rset}{\mathbb{R}}            % Reals

64: \providecommand*{\nonnegRset}{\mathbb{R}_{\scriptscriptstyle{+}}}

65:                                                % Non-negative reals

66: 

67: %% Uncomment this for page numbers.

68: \pagestyle{plain}

69: 

70: \hyphenation{%

71: %% From the AMS packages

72: acad-e-my acad-e-mies af-ter-thought anom-aly anom-alies

73: an-ti-deriv-a-tive an-tin-o-my an-tin-o-mies apoth-e-o-ses

74: apoth-e-o-sis ap-pen-dix ar-che-typ-al as-sign-a-ble as-sist-ant-ship

75: as-ymp-tot-ic asyn-chro-nous at-trib-uted at-trib-ut-able bank-rupt

76: bank-rupt-cy bi-dif-fer-en-tial blue-print busier busiest

77: cat-a-stroph-ic cat-a-stroph-i-cally con-gress cross-hatched data-base

78: de-fin-i-tive de-riv-a-tive dis-trib-ute dri-ver dri-vers eco-nom-ics

79: econ-o-mist elit-ist equi-vari-ant ex-quis-ite ex-tra-or-di-nary

80: flow-chart for-mi-da-ble forth-right friv-o-lous ge-o-des-ic

81: ge-o-det-ic geo-met-ric griev-ance griev-ous griev-ous-ly

82: hexa-dec-i-mal ho-lo-no-my ho-mo-thetic ideals idio-syn-crasy

83: in-fin-ite-ly in-fin-i-tes-i-mal ir-rev-o-ca-ble key-stroke

84: lam-en-ta-ble light-weight mal-a-prop-ism man-u-script mar-gin-al

85: meta-bol-ic me-tab-o-lism meta-lan-guage me-trop-o-lis

86: met-ro-pol-i-tan mi-nut-est mol-e-cule mono-chrome mono-pole

87: mo-nop-oly mono-spline mo-not-o-nous mul-ti-fac-eted mul-ti-plic-able

88: non-euclid-ean non-iso-mor-phic non-smooth par-a-digm par-a-bol-ic

89: pa-rab-o-loid pa-ram-e-trize para-mount pen-ta-gon phe-nom-e-non

90: post-script pre-am-ble pro-ce-dur-al pro-hib-i-tive pro-hib-i-tive-ly

91: pseu-do-dif-fer-en-tial pseu-do-fi-nite pseu-do-nym qua-drat-ic

92: quad-ra-ture qua-si-smooth qua-si-sta-tion-ary qua-si-tri-an-gu-lar

93: quin-tes-sence quin-tes-sen-tial re-arrange-ment rec-tan-gle

94: ret-ri-bu-tion retro-fit retro-fit-ted right-eous right-eous-ness

95: ro-bot ro-bot-ics sched-ul-ing se-mes-ter semi-def-i-nite

96: semi-ho-mo-thet-ic set-up se-vere-ly side-step sov-er-eign spe-cious

97: spher-oid spher-oid-al star-tling star-tling-ly sta-tis-tics

98: sto-chas-tic straight-est strange-ness strat-a-gem strong-hold

99: sum-ma-ble symp-to-matic syn-chro-nous topo-graph-i-cal tra-vers-a-ble

100: tra-ver-sal tra-ver-sals treach-ery turn-around un-at-tached

101: un-err-ing-ly white-space wide-spread wing-spread wretch-ed

102: wretch-ed-ly Eng-lish Euler-ian Feb-ru-ary Gauss-ian

103: Hamil-ton-ian Her-mit-ian Jan-u-ary Japan-ese Kor-te-weg

104: Le-gendre Mar-kov-ian Noe-ther-ian No-vem-ber Rie-mann-ian Sep-tem-ber

105: %% Added myself

106: Ba-gna-ra Zaf-fa-nel-la Par-ma

107: }

108: 

109: \begin{document}

110: 

111: %%\allowdisplaybreaks

112: 

113: \begin{frontmatter}

114: 

115: \title{The Parma Polyhedra Library: \\ Toward a Complete Set of Numerical

116: Abstractions for the Analysis and Verification

117: of Hardware and Software Systems\thanksref{th}}

118: 

119: \thanks[th]{This

120: work has been partly supported by PRIN project

121: ``AIDA: Abstract Interpretation Design and Applications.''

122: }

123: 

124: \author[Parma]{Roberto Bagnara},

125: \ead{bagnara@cs.unipr.it}

126: \author[Leeds]{Patricia M. Hill},

127: \ead{hill@comp.leeds.ac.uk}

128: \author[Parma]{Enea Zaffanella}

129: \ead{zaffanella@cs.unipr.it}

130: 

131: \address[Parma]{Department of Mathematics, University of Parma, Italy}

132: \address[Leeds]{School of Computing, University of Leeds, UK}

133: 

134: \begin{abstract}

135: Since its inception as a student project in 2001,

136: initially just for the handling (as the name implies) of convex polyhedra,

137: the \emph{Parma Polyhedra Library} has been continuously improved and

138: extended by joining scrupulous research on the theoretical foundations

139: of (possibly non-convex) numerical abstractions to a total adherence

140: to the best available practices in software development.

141: Even though it is still not fully mature and functionally complete,

142: the Parma Polyhedra Library already offers a combination of

143: functionality, reliability, usability and performance that is not

144: matched by similar, freely available libraries.

145: In this paper, we present the main features of the current version of

146: the library, emphasizing those that distinguish it from other similar

147: libraries and those that are important for applications in the field

148: of analysis and verification of hardware and software systems.

149: \end{abstract}

150: 

151: \begin{keyword}

152: Formal methods, static analysis, computer-aided verification,

153: abstract interpretation, numerical properties.

154: \end{keyword}

155: 

156: \end{frontmatter}

157: 

158: \section{Introduction}

159: 

160: The \emph{Parma Polyhedra Library} (PPL) is a collaborative project

161: started in January~2001 at the Department of Mathematics

162: of the University of Parma, Italy.

163: Since 2002, the library is actively being developed also at

164: the School of Computing of the University of Leeds, United Kingdom.

165: The PPL, that was initially limited ---as the name implies---

166: to the handling of (not necessarily topologically closed)

167: convex polyhedra \cite{BagnaraRZH02}, is now aimed at becoming

168: a truly professional, functionally complete library for the handling

169: of numeric approximations targeted at abstract interpretation and

170: computer-aided verification of hardware and software systems.

171: 

172: In this paper we briefly describe the main features of the PPL.

173: Unless otherwise stated, the description refers to version 0.9 of the

174: library, released on March 12, 2006.

175: In other cases the described features have not yet been included into

176: an official release, but are still available from the PPL's public

177: CVS repository (since development of the library takes place on that

178: repository, the PPL is always in a state of continuous release).

179: 

180: In the sequel we will compare the PPL with other libraries

181: for the manipulation of convex polyhedra.

182: These are:\footnote{We restrict ourselves to those libraries that are

183: freely available and provide the services required by applications

184: in static analysis and computer-aided verification.}

185: \begin{itemize}

186: \item

187: \emph{PolyLib} (version 5.22.1),

188: originally designed by D.~K.~Wilde \cite{Wilde93th},

189: based on an efficient C implementation of N.~V.~Chernikova's

190: algorithm \cite{Chernikova64,Chernikova65,Chernikova68}

191: written by H.~Le~Verge \cite{LeVerge92}, and further developed

192: and maintained by V.~Loechner

193: \cite{Loechner99};\footnote{\url{http://icps.u-strasbg.fr/~loechner/polylib/}.}

194: \item

195: \emph{New Polka} (version 2.1.0a), by B.~Jeannet

196: \cite{NEW-POLKA-1-1-3c};\footnote{\url{http://pop-art.inrialpes.fr/people/bjeannet/newpolka/index.html}.}

197: \item

198: the polyhedra library that comes with the \emph{HyTech} tool

199: (version 1.04f) \cite{HenzingerHW97b};\footnote{\url{http://embedded.eecs.berkeley.edu/research/hytech/}.}

200: \item

201: the \emph{Octagon Abstract Domain Library} (version 0.9.8), by A.~Min\'e

202: \cite{Mine01b,Mine05th}.\footnote{\url{http://www.di.ens.fr/~mine/oct/}.}

203: \end{itemize}

204: 

205: For reasons of space and opportunity, the paper concentrates on

206: introducing the library to prospective users.  As a consequence, we

207: assume the reader has some familiarity with the applications of

208: numerical abstractions in formal analysis and verification methods and

209: that she is not immediately concerned by the theory that lies

210: behind those abstractions.  However, the paper provides a complete

211: set of references that enable any interested reader to reconstruct

212: every detail concerning the library, the applications and the

213: relevant theory.

214: 

215: The paper is structured as follows:

216: Section~\ref{sec:abstractions} introduces the numerical abstractions

217: currently supported by the Parma Polyhedra Library;

218: Section~\ref{sec:features} describes, also by means of examples, some

219: of the most important features of the library;

220: Section~\ref{sec:efficiency} gives some indications concerning efficiency;

221: Section~\ref{sec:development-plans} illustrates the current development plans

222: for the library;

223: Section~\ref{sec:discussion} reviews some of the applications using

224: the PPL and concludes.

225: 

226: \section{Currently Supported Abstractions}

227: \label{sec:abstractions}

228: 

229: The numerical abstractions currently supported by the Parma Polyhedra

230: Library are the domains of polyhedra, bounded difference shapes,

231: octagonal shapes and grids; powersets of these using the generic

232: powerset construction; and linear programming problems.

233: For each of the supported abstractions, the library features all the

234: operators required by semantic constructions based on

235: \emph{abstract interpretation} \cite{CousotC77,CousotC79};

236: these are summarized in the following paragraphs.

237: 

238: 

239: \paragraph*{Construction}

240: The domain elements can be initialized by means of a variety of

241: constructors; in particular, they can be defined to be a vector space

242: for a specified number of dimensions ---each dimension representing

243: some concrete entity relevant for the particular analysis---

244: indicating that at this stage nothing is known about the entities, or

245: the empty abstraction (again for a given number of dimensions),

246: describing an inconsistent (unreachable) state.

247: An element can also be initialized by means of \emph{constraints},

248: specifying conditions its points must satisfy; alternatively, it can

249: be described by \emph{generators}, that are meant to be parametrically

250: combined so as to describe all of its points.

251: New elements can also be constructed by copying an existing element in

252: the same abstraction.

253: 

254: \paragraph*{Refinement and Expansion}

255: Any domain element can be refined by the addition of further constraints

256: its points must satisfy, thereby improving the precision of the description:

257: a typical application of refinement is to model the effect of

258: conditional guards in if-then-else and while-loop statements.

259: The expansion operators allow users to add new generators

260: so as to expand the set of points the element must contain;

261: these may be used, for instance, to ``forget'' some information

262: regarding a space dimension, so as to model arbitrary input by the user.

263: 

264: \paragraph*{Upper and Lower Bounds}

265: It is often useful to compute an upper or lower bound of two domain

266: elements so as to obtain a correct approximation of their union or

267: intersection.

268: For example, an analyzer could use an upper bound operator

269: to combine approximations

270: that have been computed along the alternative branches of an

271: if-then-else statement while

272: lower bound operators are needed, in combination with conversion operators

273: (see below), when conjunctively merging different approximations computed

274: along the same set of computation paths.

275: 

276: \paragraph*{Affine Images and Preimages}

277: A common form of statement in an imperative language

278: is the assignment of an affine expression to a program variable.

279: Their semantics can be modeled by

280: images (in a forward analysis) and/or

281: preimages (in a backward analysis) of affine transformations

282: on domain elements.

283: All domains fully support the efficient (and possibly approximate)

284: computation of affine images and preimages.

285: Also available are generalizations of these operators,

286: useful for approximating more complex assignment statements

287: (e.g., to model constrained nondeterministic assignments or

288: when a non-linear expression can be bounded from below and/or above

289: by affine expressions).

290: 

291: \paragraph*{Changing Dimensions}

292: An analyzer needs to be able to add, remove, and more generally reorganize

293: the space dimensions that are associated with the values of the concrete

294: entities it is approximating. The simple addition and removal of dimensions

295: is often needed at the entry and exit points of various kinds of

296: programming contexts, such as declaration blocks where concrete entities

297: (modeled by some of the space dimensions) may be local to the block.

298: More complex operators are useful to support the integration of the

299: results computed using different abstractions, that typically provide

300: information about different sets of concrete entities.

301: In the simplest case, when the abstractions are of the same kind but

302: provide information about disjoint sets of concrete entities, it is

303: enough to \emph{concatenate} the two abstract elements into a new one.

304: In more complex cases, when the described sets of concrete entities

305: have an overlap, the space dimensions of one of the abstract elements

306: need to be reconciled with those of the other, allowing for a correct

307: integration of the information.

308: This can be obtained by efficiently \emph{mapping} the space dimensions

309: according to a (partial) injective function.

310: The library also supports the \emph{folding} (and unfolding) of space

311: dimensions, which is needed to correctly and efficiently

312: summarize the information regarding collections of concrete

313: entities~\cite{GopanDMDRS04}.

314: 

315: \paragraph*{Conversion}

316: Non-trivial analyses are typically based on a combination of domains.

317: It is therefore important to be able to safely and efficiently convert

318: between different abstractions. These conversions enable, for

319: instance, the combination of domain elements

320: representing different kinds of information,

321: implementing so-called \emph{reduction} operators. Another important

322: application is the dynamic control of the precision/efficiency ratio:

323: in order to gain efficiency in the analysis of a specific context,

324: an element of a relatively precise domain can temporarily be converted into

325: an element of a weaker domain and then back to the stronger

326: abstraction on exit from that context.

327: 

328: \paragraph*{Comparison}

329: The analysis of a program fragment is implemented by computing an

330: over-approximation of its semantics.  Since the latter is usually

331: modeled as the least fixpoint of a continuous operator, a safe

332: analysis typically needs to iteratively compute an over-approximation

333: of this fixpoint.  Therefore, a suitable lattice-theoretic comparison

334: operator is needed so as to check for the convergence of the analysis.

335: Comparison operators are also useful in selected contexts so as to

336: efficiently predict whether or not some precision improving techniques

337: (e.g., reductions, widening variants and so on) are applicable.  For

338: all of the reasons above, each domain provides three different

339: comparison operators checking, respectively, equality, containment and

340: strict containment.

341: 

342: \paragraph*{Widening}

343: Most of the domains supported by the library admit \emph{infinite

344: ascending chains}.  These are infinite sequences of domain elements

345: such that every element in the sequence is contained in the element

346: that follows it. With these characteristics,

347: the fixpoint computations upon which abstract interpretation analysis

348: techniques are based could be non-terminating.

349: For this reason, the domains can be so employed

350: only in conjunction with appropriate mechanisms for enforcing and/or

351: accelerating the convergence of fixpoint computations: widening

352: operators \cite{CousotC76,CousotC77,CousotC92fr,CousotC92plilp}

353: provide a simple and general characterization for such

354: mechanisms.%

355: \footnote{Operators that do not provide a strict convergence guarantee

356: are more properly called \emph{extrapolation} operators.}

357: The PPL offers also several variations of the available widenings:%

358: \footnote{Some of these variations are extrapolation operators,

359: as the guarantee of convergence is conditional on the way they are used.}

360: widening ``with tokens'' (an improvement to the widening delay technique

361: proposed in \cite{Cousot81});  and widening ``up to''

362: \cite{Halbwachs93,HalbwachsPR97} (a technique whereby constraints that

363: are judged to be important by the application can be preserved from the

364: action of the widening).

365: 

366: \paragraph*{Other Operators}

367: The library offers many other operators for use in a variety of

368: more specialized contexts.

369: For instance, before performing a non-trivial domain combination,

370: an analyzer may need information

371: about a particular domain element (such as, checking whether it denotes

372: the empty set or the whole vector space; the

373: dimension of the vector space; the affine dimension of the element;

374: its relation with respect to a given constraint or generator, and so

375: on). Another operator supported by the library is the

376: \emph{difference} operator, which computes the smallest domain element

377: that contains the set difference of two elements; this is exploited in the

378: implementation of the finite powerset widening operator proposed

379: in~\cite{BagnaraHZ06STTT}. The library also provides

380: the \emph{time-elapse} operator used to model hybrid systems

381: \cite{HalbwachsPR97}.

382: 

383: The following sections briefly describe each of the supported domains.

384: The emphasis here is on the features that are unique to the PPL.  The

385: reader is referred to the cited literature and to the library's

386: documentation \cite{PPL-DEVREF-0-9,PPL-USER-0-9} for all the details.

387: 

388: \subsection{Closed and Not Necessarily Closed Polyhedra}

389: 

390: The Parma Polyhedra Library supports computations on the abstract

391: domain of convex polyhedra \cite{CousotH78,Halbwachs79th}.

392: The PPL implements both the abstract domain of

393: topologically \emph{closed convex polyhedra} (briefly called \emph{C polyhedra}

394: and implemented by class \verb+C_Polyhedron+)

395: and the abstract domain of \emph{not necessarily closed convex polyhedra}

396: (\emph{NNC polyhedra} for short, class \verb+NNC_Polyhedron+).

397: In both cases, polyhedra are represented and manipulated using the

398: \emph{Double Description} (DD) method of Motzkin et al.\ \cite{MotzkinRTT53}.

399: In this approach, a closed convex polyhedron can be specified in two ways,

400: using a \emph{constraint system} (class \verb+Constraint_System+)

401: or a \emph{generator system} (class \verb+Generator_System+):

402: the constraint system is a finite set of linear equality or inequality

403: constraints (class \verb+Constraint+);

404: the generator system is a finite set of different kinds of vectors,

405: collectively called \emph{generators},

406: which are rays and points of the polyhedron (class \verb+Generator+).

407: An example of double description is depicted

408: in Figure~\ref{fig:polyhedron-double-description}: the polyhedron

409: represented by the shaded region can be represented by the set of vectors

410: satisfying the constraints or, equivalently, by the set

411: \[

412:   \{\,

413:     \pi_1 \mathbf{p}_1 + \pi_2 \mathbf{p}_2

414:       + \rho_1 \mathbf{r}_1 + \rho_2 \mathbf{r}_2 \in \Rset^2

415:   \mid

416:     \pi_1, \pi_2, \rho_1, \rho_2 \in \Rset_+, \pi_1 + \pi_2 = 1

417:   \,\},

418: \]

419: where

420: $\mathbf{p}_1 = \left( \begin{smallmatrix}4 \\1\end{smallmatrix} \right)$,

421: $\mathbf{p}_2 = \left( \begin{smallmatrix}1 \\4\end{smallmatrix} \right)$,

422: $\mathbf{r}_1 = \left( \begin{smallmatrix}1 \\2\end{smallmatrix} \right)$,

423: $\mathbf{r}_2 = \left( \begin{smallmatrix}2 \\1\end{smallmatrix} \right)$,

424: and $\Rset_+$ is the set of non-negative real numbers.

425: In words, each vector can be obtained by adding a non-negative combination

426: of the rays and a convex combination of the points.

427: 

428: \begin{figure}

429: \centering

430: \begin{minipage}{8cm}

431: \[

432: \psset{xunit=2.4mm,yunit=2.4mm,runit=2.4mm}

433: \psset{origin={-0.5,-0.5}}

434: \pspicture*[](-2,-2)(25,25)

435: \pspolygon[fillstyle=solid,fillcolor=green,linecolor=green](1,4)(11,24)(24,24)(24,11)(4,1)

436: \psline[linecolor=blue](-2,7)(7,-2)

437: \psline[linecolor=blue](-1.5,-1)(11,24)

438: \psline[linecolor=blue](-1,-1.5)(24,11)

439: \psdots*[linecolor=red,dotstyle=square*,dotsize=0.6 0.6](1,4)(4,1)

440: \psline[linecolor=red]{->}(2.5,2.5)(4.5,6.5)

441: \psline[linecolor=red]{->}(2.5,2.5)(6.5,4.5)

442: \psline{->}(-2,0)(24,0)

443: \psline{->}(0,-2)(0,24)

444: \rput(23,-0.8){$x$}

445: \rput(-0.8,23){$y$}

446: \endpspicture

447: \]

448: \end{minipage}%

449: %

450: \begin{minipage}{5.7cm}

451: \begin{align*}

452: &\begin{cases}

453:   \blue{x + y \geq 5} \\

454:   \blue{x - 2y \leq 2} \\

455:   \blue{y - 2x \leq 2}

456: \end{cases} \\[1cm]

457: &\begin{cases}

458:   \red{\text{points: } \bigl\{ (4, 1), (1, 4) \bigr\}} \\

459:   \red{\text{rays: } \{ (1, 2), (2, 1) \}}

460: \end{cases}

461: \end{align*}

462: \end{minipage}

463: \caption{The double description method for polyhedra}

464: \label{fig:polyhedron-double-description}

465: \end{figure}

466: 

467: Implementation of convex polyhedra using the DD method offer some important

468: advantages to analysis and verification applications.

469: The first one is due to the ``mix'' of operations such applications require:

470: some of them are more efficiently performed on the representation with

471: constraints.  This is the case for the addition of constraints and for

472: the intersection, which is simply implemented as the union of constraint

473: systems, and for deciding whether a generator is subsumed or not by a

474: polyhedron (e.g., to decide whether a point is inside or outside).

475: Some operations are instead more efficiently performed on generators:

476: computing the convex polyhedral hull (just by taking the union of generator

477: systems), adding individual generators

478: (e.g., the addition of the rays

479: $\mathbf{r} = \left( \begin{smallmatrix}1 \\0\end{smallmatrix} \right)$ and

480: $-\mathbf{r}$ to the set of rays for the polyhedron in

481: Figure~\ref{fig:polyhedron-double-description}

482: is the easiest way to ``forget'' all the information concerning the

483: space dimension~$x$),

484: projection onto designated dimensions, deciding whether

485: the space defined by a constraint is disjoint, intersects or includes

486: a given polyhedron, finiteness/boundedness tests

487: (a polyhedron is finite/bounded if and only if it has no rays among its

488: generators),

489: and the \emph{time-elapse} operator

490: of~\cite{HalbwachsPR94,HalbwachsPR97}.

491: There are also important operations, such as the inclusion and equality tests

492: and the widenings, that are more efficiently performed

493: when \emph{both} representations are available.

494: Systems of constraints and generators enjoy a quite strong

495: and useful duality property.

496: Very roughly speaking, the constraints of a polyhedron are (almost)

497: the generators of the \emph{polar} \cite{NemhauserW88,StoerW70} of the

498: polyhedron, the generators of a polyhedron are (almost) the

499: constraints of the polar of the polyhedron, and the polar of the polar

500: of a polyhedron is the polyhedron itself.

501: This implies that computing constraints from generators is the same

502: problem as computing generators from constraints.

503: The algorithm of N.~V.~Chernikova \cite{Chernikova64,Chernikova65,Chernikova68}

504: (later improved by H.~Le~Verge \cite{LeVerge92}

505: and by K.~Fukuda and A.~Prodon \cite{FukudaP96})

506: solves both problems yielding a minimized system and can be implemented

507: so that the source system is also minimized in the process.

508: This is basically the algorithm employed by PolyLib, New Polka

509: and the Parma Polyhedra Library.

510: It is worth noticing that it is not restrictive to express the coefficients

511: of constraints and rays by integer numbers, as using rational numbers

512: would not result in increased expressivity (but would have a negative

513: impact on efficiency).  For points, a common integer denominator suffices.%

514: \footnote{The correctness requirements of applications in

515: the field of system's analysis and verification prevent the adoption

516: of floating-point coefficients, since any rounding error on the wrong

517: side can invalidate the overall computation.  For domains as

518: complicated as that of polyhedra, the correct, precise and reasonably

519: efficient handling of floating-point rounding errors is an open

520: issue.}

521: 

522: Restricting the attention to convex polyhedra, two of the main innovations

523: introduced by the PPL are the complete handling of NNC polyhedra and the

524: introduction of a new widening operator.

525: Apart from the PPL, the only libraries---among those that provide the

526: services required by applications in static analysis and computer-aided

527: verification---that support NNC polyhedra are the already mentioned New Polka

528: and the library by N.~Halbwachs, A.~Kerbrat and Y.-E.~Proy called, simply,

529: \emph{Polka} \cite{HalbwachsKP95}.  The Polka library, however, is not

530: available in source format and binaries are distributed under rather

531: restrictive conditions (until about the year 1996 they could be freely

532: downloaded), so our knowledge of it is as given in \cite{HalbwachsKP95},

533: the programmer's manual in a package that includes the actual library.

534: The support provided by Polka and New Polka for NNC polyhedra is

535: incomplete, incurs avoidable inefficiencies and leaves the client

536: application with the non-trivial task of a correct interpretation of

537: the results.  In particular, even though an NNC polyhedron can be

538: described by using constraint systems that may contain strict inequalities,

539: the Polka and New Polka libraries lack a corresponding extension

540: for generator systems.

541: In contrast, the PPL implements the proposal put forward in

542: \cite{BagnaraHZ05FAC}, whereby the introduction of \emph{closure points}

543: as a new kind of generator, allows a clean user interface,

544: symmetric to the constraint system interface for NNC polyhedra,

545: that is decoupled from the implementation.

546: As explained in detail in \cite{BagnaraHZ05FAC}, a user of the PPL

547: is fully shielded from implementation details such as the extra

548: $\epsilon$ dimension that users of the other libraries have to carefully

549: take into account.  Another feature that is unique to the PPL is

550: the support for the minimization of the descriptions of an NNC polyhedron:

551: we refer the interested reader to \cite{BagnaraHZ05FAC} for a precise

552: account of the impact this new feature has on performance and usability.

553: 

554: The original widening operator proposed by Cousot and Halbwachs

555: \cite{CousotH78,Halbwachs79th} is termed \emph{standard widening} since,

556: for 25 years, all analysis and verification tools that employed convex

557: polyhedra also employed that operator.

558: Nonetheless, there was an unfulfilled demand for more precise widening

559: operators.  The Parma Polyhedra Library, besides the standard

560: widening, offers the new widening proposed in \cite{BagnaraHRZ05SCP}:

561: on a single application this is always more precise than the standard

562: widening.  As these widenings are not monotonic, increased precision

563: on a single application does not imply increased precision on the

564: final result of the analysis.  In practice, however, an overall

565: increase of precision is almost always achieved

566: \cite{BagnaraHRZ05SCP}.

567: 

568: Both widenings can be improved, as said before, by applying the

569: ``widening with tokens'' delay strategy or the ``widening up-to''

570: technique; moreover, ``bounded'' extrapolation operators are available

571: that provide additional precision guarantees over the widenings upon

572: which they are built.

573: 

574: \subsection{Bounded Difference Shapes}

575: \label{sec:bounded-difference-shapes}

576: 

577: By restricting to particular subclasses of linear constraints, it is

578: possible to obtain domains that are simpler and computationally more

579: efficient than the one of convex polyhedra.

580: One possibility, which has a long tradition in computer

581: science~\cite{Bellman57}, is to only consider

582: \emph{potential constraints}, also known as \emph{bounded differences}:

583: these are restricted to take the form $v_i - v_j \leq d$ or $\pm v_i \leq d$,

584: where $v_i$ and $v_j$ are variables and $d$, the \emph{inhomogeneous term},

585: belongs to some computable number family.

586: Systems of bounded differences have been used

587: by the artificial intelligence community as a way to reason about

588: temporal quantities \cite{AllenK85,Davis87},

589: as well as by the model checking community as an

590: efficient yet precise way to model and propagate timing requirements

591: during the verification of various kinds of concurrent systems

592: \cite{Dill89,LarsenLPY97}.

593: In the abstract interpretation field, the idea of using an abstract

594: domain of bounded differences was put forward in \cite{Bagnara97th}

595: and the first fully developed application of bounded differences

596: in this field can be found in~\cite{ShahamKS00}.

597: Possible representations for finite systems of bounded differences are

598: matrix-like data structures called \emph{difference-bound matrices}

599: (DBM) \cite{Bellman57} and weighted graphs called \emph{constraint networks}

600: \cite{Davis87}.  These representations, however, have a ``syntactic'' nature:

601: they encode sets of constraints rather than geometric shapes.

602: As pointed out in \cite{BagnaraHMZ05} this nature has several drawbacks,

603: the most important one being that natural extrapolation operators

604: do not provide a convergence guarantee, that is, they are not widenings.

605: This results into an extra burden on the client application, which has

606: to take into account the implementation details and use the domain elements

607: with care so as to avoid non-termination of the analysis.

608: 

609: In order to overcome the difficulties mentioned above and to continue

610: pursuing a complete separation between interface (which must be natural

611: and easy to use) and implementation (which must be efficient and robust),

612: the Parma Polyhedra Library offers the ``semantic'' domain of

613: \emph{bounded difference shapes}.

614: A bounded difference shape is nothing but a geometric shape, that is,

615: a convex polyhedron: its internal representation needs not concern

616: (and, in fact, is completely hidden from) the client application.

617: The class template implementing this domain in the PPL is

618: \verb+BD_Shape<T>+, where the class template type parameter \verb+T+

619: defines the family of numbers that are used to (correctly) approximate

620: the inhomogeneous terms of bounded differences.

621: The value of \verb+T+ may be one of the following:

622: \begin{itemize}

623: \item

624: a bounded precision native integer type (that is,

625: from \verb+signed+ \verb+char+ to \verb+long+ \verb+long+

626: and from \verb+int8_t+ to \verb+int64_t+);

627: \item

628: a bounded precision floating point type (\verb+float+, \verb+double+

629: or \verb+long+ \verb+double+);

630: \item

631: an unbounded integer or rational type, as provided by GMP

632: (\verb+mpz_class+ or \verb+mpq_class+).

633: \end{itemize}

634: Among other things, PPL's \verb+BD_Shape<T>+ offers the proper widening

635: operator defined in \cite{BagnaraHMZ05} and a user interface that matches

636: the interfaces of the general polyhedra classes \verb+C_Polyhedron+

637: and \verb+NNC_Polyhedron+.

638: 

639: \subsection{Octagonal Shapes}

640: 

641: Another restricted class of linear constraints was introduced

642: in~\cite{BalasundaramK89}.  These are of the form

643: $a v_i + b v_j \leq d$, where $a, b \in \{-1, 0, +1\}$ and $d$

644: belongs to some computable number family.

645: Systems of such constraints were called \emph{simple sections}

646: in~\cite{BalasundaramK89} and have been given the structure of

647: an abstract domain by A.~Min\'e \cite{Mine01b}.

648: The resulting \emph{octagon abstract domain} has, due to its syntactic

649: nature, the same problems outlined in the previous section.

650: This is why, as explained in detail in \cite{BagnaraHMZ05},

651: the Parma Polyhedra Library offers a semantic domain of

652: \emph{octagonal shapes}, for which it provides a widening operator.

653: This is implemented by the class template

654: \verb+Octagonal_Shape<T>+, where the class template type parameter \verb+T+

655: can be instantiated as for bounded difference shapes.\footnote{Support for

656: octagonal shapes has not yet been included into a formal release.  It is

657: however complete and available in the PPL's public CVS repository.}

658: Another feature of this class is that its implementation uses

659: the strong closure algorithm introduced in \cite{BagnaraHMZ05},

660: which has lower complexity than the one used in the

661: Octagon Abstract Domain Library%

662: \footnote{Until at least version 0.9.8.} \cite{Mine01b,Mine05th}.

663: 

664: \subsection{Grids}

665: 

666: Given $a_1$, \dots,~$a_n$, $b$, $f \in \Zset$,

667: the \emph{linear congruence relation}

668: $a_1v_1 + \cdots + a_nv_n \equiv_f b$

669: denotes the subset of $\Rset^n$

670: given by

671: \[

672:   \biggl\{\,

673:     \langle q_1, \ldots, q_n \rangle \in \Rset^n

674:   \bigm|

675:     \exists \mu \in \Zset \st

676:       \sum_{i=1}^n a_iq_i = b + \mu f

677:   \,\biggr\};

678: \]

679: when $f \neq 0$, the relation is said to be \emph{proper};

680: when $f = 0$, the relation is equivalent to (i.e., it denotes the same

681: hyperplane as) $a_1v_1 + \cdots + a_nv_n = b$.

682: A \emph{congruence system} is a finite set of congruence relations

683: and a \emph{grid} is any subset of $\Rset^n$ whose elements

684: satisfy all the congruences of such a system.

685: The \emph{grid domain} is the set of all such grids.

686: 

687: \begin{figure}

688: \centering

689: %\setlength{\unitlength}{0.6pt}%

690: \begin{minipage}{8cm}

691: \[

692: \psset{xunit=1.1cm,yunit=1.1cm,runit=1.1cm}

693: \psset{origin={1,0.3}}

694: \pspicture*[](-3.5,0)(3.6,6.2)

695: %

696: \psline{->}(-2.2,3)(3.6,3)

697: \psline{->}(0,0.5)(0,6.2)

698: \rput(2.35,2.45){$x$}

699: \rput(-1.3,5.65){$y$}

700: %

701: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

702: (-2,0.7)(-2,5.8)

703: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

704: (-1,0.7)(-1,5.8)

705: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

706: (0,0.7)(0,5.8)

707: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

708: (1,0.7)(1,5.8)

709: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

710: (2,0.7)(2,5.8)

711: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

712: (3,0.7)(3,5.8)

713: %

714: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

715: (1.4,5.8)(3.2,4.9)

716: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

717: (-0.6,5.8)(3.2,3.9)

718: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

719: (-2.2,5.6)(3.2,2.9)

720: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

721: (-2.2,4.6)(3.2,1.9)

722: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

723: (-2.2,3.6)(3.2,0.9)

724: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

725: (-2.2,2.6)(1.6,0.7)

726: \psline[linecolor=blue,linestyle=dashed,dash=6pt 2pt]

727: (-2.2,1.6)(-0.4,0.7)

728: %

729: \psdots*[linecolor=red,dotstyle=square,dotsize=0.15 0.15]

730: (-2,1.5)(-2,2.5)(-2,3.5)(-2,4.5)(-2,5.5)

731: (-1,1)(-1,2)(-1,3)(-1,4)(-1,5)

732: (0,1.5)(0,2.5)(0,3.5)(0,4.5)(0,5.5)

733: (1,1)(1,2)(1,3)(1,4)(1,5)

734: (2,1.5)(2,2.5)(2,3.5)(2,4.5)(2,5.5)

735: (3,1)(3,2)(3,3)(3,4)(3,5)

736: %

737: \psdots*[linecolor=red,dotstyle=square*,dotsize=0.15 0.15]

738: (1,3)(3,3)(2,3.5)

739: \psline[linecolor=red]{->}(1,3)(2.92,3)

740: \psline[linecolor=red]{->}(1,3)(1.92,3.475)

741: \endpspicture

742: \]

743: \end{minipage}%

744: %

745: \begin{minipage}{5.7cm}

746: \begin{align*}

747: &\begin{cases}

748:   \blue{x \equiv_2 0} \\

749:   \blue{x + 2y \equiv_4 2}

750: \end{cases} \\[1cm]

751: &\begin{cases}

752:   \red{\text{points: } \bigl\{ (2, 0), (6, 0), (4, 1) \bigr\}}

753: \end{cases} \\[1cm]

754: &\begin{cases}

755:   \red{\text{points: } \bigl\{ (2, 0) \bigr\}} \\

756:   \red{\text{parameters: } \bigl\{ (4, 0), (2, 1) \bigr\}} \\

757: \end{cases}

758: \end{align*}

759: \end{minipage}

760: \caption{The double description method for grids}

761: \label{fig:grid-double-description}

762: \end{figure}

763: 

764: An example of grid is given in Figure~\ref{fig:grid-double-description},

765: where the solutions of the congruence relations are given by the dashed

766: lines and the grid elements by the (filled and unfilled) squares.

767: The figure shows also that there is an alternative way of describing

768: the same grid: if we call the points marked by the filled squares

769: $\mathbf{p}_1 = \left( \begin{smallmatrix}2 \\0\end{smallmatrix} \right)$,

770: $\mathbf{p}_2 = \left( \begin{smallmatrix}6 \\0\end{smallmatrix} \right)$

771: and

772: $\mathbf{p}_3 = \left( \begin{smallmatrix}4 \\1\end{smallmatrix} \right)$,

773: we can see that the grid is given by

774: \begin{equation}

775: \label{eq:affine-integral-combination}

776:   \{\,

777:     \pi_1 \mathbf{p}_1 + \pi_2 \mathbf{p}_2 + \pi_3 \mathbf{p}_3 \in \Rset^2

778:   \mid

779:     \pi_1, \pi_2, \pi_3 \in \Zset, \pi_1 + \pi_2 + \pi_3 = 1

780:   \,\}.

781: \end{equation}

782: We say that the set of \emph{points}

783: $\{ \mathbf{p}_1, \mathbf{p}_2, \mathbf{p}_3 \}$ \emph{generates}

784: the grid.

785: Some of these generating points can be replaced by \emph{parameters}

786: that give the direction and spacing for the neighboring points.

787: Specifically, by subtracting the point $\mathbf{p}_1$ from each of the

788: other two generating points $\mathbf{p}_2$ and $\mathbf{p}_3$, we obtain

789: the parameters

790: $\mathbf{q}_2 = \left( \begin{smallmatrix}4 \\0\end{smallmatrix} \right)$

791: and

792: $\mathbf{q}_3 = \left( \begin{smallmatrix}2 \\1\end{smallmatrix} \right)$

793: and can now express the grid as

794: \[

795:   \{\,

796:     \mathbf{p}_1 + \pi_2 \mathbf{q}_2 + \pi_3 \mathbf{q}_3 \in \Rset^2

797:   \mid

798:     \pi_2, \pi_3 \in \Zset

799:   \,\}.

800: \]

801: Notice that, in the generator representation for grids, points and parameters

802: can have rational, non integer coordinates.

803: 

804: The domain of grids, as briefly described above, has been introduced

805: by P.~Granger \cite{Granger91,Granger97} and its design has been

806: completed in \cite{BagnaraDHMZ06a,BagnaraDHMZ06b}

807: by including refined algorithms and new operators

808: for affine images, preimages and their generalizations, grid-difference

809: and widening.

810: The Parma Polyhedra Library includes the first truly complete

811: implementation of this abstract domain by means of the \verb+Grid+ class.

812: Congruence relations and systems thereof are realized by the classes

813: \verb+Congruence+ and \verb+Congruence_System+, and likewise

814: for generators with the classes \verb+Grid_Generator+,

815: and \verb+Grid_Generator_System+.

816: 

817: A more restricted domain, the domain of \emph{integral lattices}

818: has been partly implemented in PolyLib~\cite{Loechner99}

819: following the approach in~\cite{QuintonRR96,QuintonRR97}.

820: An integral lattice in dimension $n$ is the grid generated by

821: the affine integral combination

822: ---as in \eqref{eq:affine-integral-combination}---

823: of exactly $n+1$ affinely independent points that are additionally

824: bound to have integer coordinates.

825: These restrictions have the consequences that only the generator representation

826: is supported and, as explained in \cite{BagnaraDHMZ06a,BagnaraDHMZ06b},

827: the reduced expressivity

828: has an impact on the possibility to solve concrete analysis problems.

829: The implementation of the domain of integral lattices in PolyLib is

830: incomplete in the sense that it misses domain operators such as

831: the join. Instead, it provides a union operator

832: which, given two lattices returns a \emph{set} of lattices

833: representing the precise set union of the points of the given lattices.

834: Similarly the difference operation on a pair of lattices

835: returns a set of lattices whose union contains the exact

836: set difference of their points.

837: Moreover, although image and preimage operators are supported

838: by PolyLib, as the integral lattice must be full dimensional,

839: only invertible image operators are allowed.

840: 

841: \subsection{Powersets}

842: 

843: For applications requiring a high degree of precision, the Parma Polyhedra

844: Library provides a generic implementation of the \emph{finite powerset}

845: construction \cite{Bagnara98SCP,BagnaraHZ06STTT}.

846: This upgrades an abstract domain into a refined one where finite

847: disjunctions of non redundant elements are precisely representable.

848: The construction is implemented generically by the class template

849: \verb+Powerset<D>+, where the type parameter \verb+D+ must provide

850: about ten methods and operators implementing, among other things,

851: an entailment predicate and operators for obtaining an upper bound

852: and the ``meet'' of two given elements.  No other requirements are

853: imposed and, in fact, the test suite of the PPL includes a program

854: where \verb+Powerset<D>+ is instantiated with a non numerical domain.

855: 

856: The class template \verb+Pointset_Powerset<PS>+ provides a specialization

857: of class \verb+Powerset<D>+ that is suitable for the instantiation with the

858: ``semantic'' numerical domains of the PPL: (C or NNC) polyhedra, bounded

859: difference shapes, octagonal shapes, grids

860: and combinations thereof.

861: A most notable and, at the time of writing, unique feature of this

862: implementation is the provision ---in addition to the extrapolation

863: operator proposed in \cite{BultanGP99}--- of provably correct,

864: \emph{certificate-based} widening operators that lift the widening operators

865: defined on the underlying domain \verb+PS+ \cite{BagnaraHZ06STTT}.

866: 

867: \subsection{Linear Programming Problems}

868: \label{sec:linear-programming-problems}

869: 

870: The library includes a Linear Programming (LP) solver based

871: on the simplex algorithm and using exact arithmetic.

872: Note that the absence of rounding errors is essential for most

873: (if not all) of the intended applications.

874: Since it is common practice to solve an LP problem

875: by exploiting duality results, correctness may be lost even if

876: \emph{controlled rounding} is used; this is because a feasible but possibly

877: non-optimal solution for the dual of an LP problem may actually correspond

878: to an unfeasible solution for the original LP problem.

879: 

880: The LP solver interface allows for both satisfiability checks

881: and optimization of linear objective functions.

882: A limited form of incrementality allows for the efficient re-optimization

883: of an LP problem after modification of the objective function.

884: Ongoing implementation work is focusing on improving the

885: efficiency of the solver as well as providing better support

886: for incremental computations, so as to also allow for the efficient

887: re-optimization of the LP problem after a modification of the

888: feasible region caused by the addition of further constraints.%

889: \footnote{The incremental LP solver has not yet been included into

890: a formal release.  It is however complete and available in

891: the PPL's public CVS repository.}

892: 

893: \section{Main Features}

894: \label{sec:features}

895: 

896: In this section we will briefly review the main features of the Parma

897: Polyhedra Library.  We will focus on usability, on the absence of

898: arbitrary limits due to the use of fully dynamic data structures,

899: on some of the measures that contribute to the library's robustness,

900: on the support for resource-bounded computations, on the possibility

901: to use machine integer coefficients without compromising correctness,

902: on portability and on the availability of complete documentation.

903: 

904: \subsection{Usability}

905: 

906: By ``usability'' of the Parma Polyhedra Library we actually mean two things:

907: \begin{enumerate}

908: \item

909: that the library provides natural, easy to use interfaces that can be used,

910: even by the non expert, to quickly prototype an application;

911: \item

912: that, nonetheless, the library and its interfaces provide all the

913: functionalities that allow their use in the development of professional,

914: reliable applications.

915: \end{enumerate}

916: In other words, simplicity of the interfaces has not been obtained

917: with simplistic solutions or by the omission of functionalities.

918: 

919: As mentioned before particular care has been taken (to the point of

920: developing the necessary theoretical concepts) in the complete

921: decoupling of the user interfaces from all implementation details.

922: So, the internal representation of, say, constraints, congruences,

923: generators and systems thereof need not concern the client application.

924: All the user interfaces, whatever language they interface to,

925: refer to high-level concepts

926: and never to their possible implementation in terms of vectors, matrices

927: or other data structures.  For instance, unlike PolyLib and

928: New Polka, implementation devices (such as so-called

929: \emph{positivity constraints} \cite{Wilde93th}

930: or \emph{$\epsilon$-representations} \cite{BagnaraHZ05FAC,HalbwachsPR94})

931: never surface at the user level and need not concern the client

932: application.  As another example, a user of the Octagon Abstract Domain

933: Library must know that octagons are represented there by means of

934: difference-bound matrices, that some of the operations on octagons

935: do ``close'' these matrices, and that one argument to the widening

936: is better closed for improved accuracy while the other should \emph{not}

937: be closed as this would prevent convergence.

938: 

939: The Parma Polyhedra Library currently offers, besides the \Cplusplus{}

940: interface, a portable Prolog interface and a C interface.

941: The Prolog interface is ``portable'' in that it supports (despite the

942: lack of standardization of Prolog foreign language interfaces) six

943: major Prolog systems: Ciao, GNU Prolog, SWI-Prolog, SICStus, XSB and

944: YAP.

945: The C interface is particularly important, as it allows to interface

946: the PPL with almost anything else: for example, third parties have

947: already built interfaces for Haskell, Java and Objective Caml.

948: The design of the interfaces to directly supported languages has been

949: focused on ensuring that programmers can use the library following the most

950: natural programming style in \emph{that} language.

951: As a simple example, in the appropriate contexts, `\texttt{X~<~5*Z}'

952: and `\texttt{X~+~2*Y~+~5*Z~>=~7}' is valid syntax expressing

953: a strict and a non-strict inequality, both in the \Cplusplus{}

954: and the Prolog interfaces.  This can be done because both languages

955: allow to override (or freely interpret) operators and provide

956: exceptions as a powerful method of reporting run-time errors.

957: Here is how a NNC polyhedron in a space of dimension~$3$ can be created

958: using the \Cplusplus{} interface:

959: %

960: \bigskip

961: \lstset{language=C++}

962: {\small

963: \begin{lstlisting}[frame=lines]

964: 

965: #include <ppl.hh>

966: 

967: namespace PPL = Parma_Polyhedra_Library;

968: 

969:   ...

970:   PPL::Variable X(0);

971:   PPL::Variable Y(1);

972:   PPL::Variable Z(2);

973:   PPL::NNC_Polyhedron ph(3, PPL::UNIVERSE);

974:   ph.add_constraint(X + 2*Y + 5*Z >= 7);

975:   ph.add_constraint(X < 5*Z);

976:   ...

977: \end{lstlisting}

978: } % \small

979: %

980: And here is how the same polyhedron can be created

981: using the Prolog interface:

982: %

983: \newpage

984: \lstset{language=Prolog}

985: {\small

986: \begin{lstlisting}[frame=lines]

987: 

988:   ...

989:   numbervars([X, Y, Z], 0, _),

990:   ppl_new_NNC_Polyhedron_from_constraints(

991:     [X + 2*Y + 5*Z >= 7, X < 5*Z],

992:     PH

993:   ),

994:   ...

995: \end{lstlisting}

996: } % \small

997: %

998: In standard C things are more complicate as the language syntax does not

999: allow to represent, say, constraints as easily.\footnote{Unless one

1000: represents them with strings.  While a string-based interface is

1001: certainly possible, we do not believe it would make things simpler:

1002: strings would have to be parsed at run-time and parsing errors would

1003: have to be properly handled.}

1004: Thus, in order to build constraints the C application will have to build

1005: the linear expressions occurring in them and the memory used to hold these

1006: intermediate data structures will have to be explicitly managed,

1007: unless a conservative garbage collector is used.

1008: Moreover, lack of exceptions means that non-trivial error detection

1009: and handling will demand significantly more effort in C than in \Cplusplus{}

1010: or Prolog (\emph{all} the functions of the C interface return an \verb+int+:

1011: a negative value indicates an error has occurred).

1012: The best approach to development using the C interface is to begin

1013: by developing a layer of interface functions that are suited to

1014: the application at hand:

1015: the PPL's C interface provides all the required services.

1016: 

1017: Still on the subject of ease of use, the numeric abstractions provided

1018: by the library provide similar interfaces. A high degree of

1019: integration is obtained through the adoption of common data types and

1020: the availability of methods specifically designed for

1021: interoperability.

1022: As a consequence, the specification and implementation of

1023: new abstractions and tools can be easily obtained by composition

1024: of the available services.

1025: As a simple example, the code in Listing~\ref{lst:lp_solver} is

1026: exploiting the LP solver capabilities to efficiently compute (and

1027: print) all the upper bounds for the variables corresponding to the

1028: dimensions of a closed polyhedron.

1029: 

1030: \lstset{language=[ISO]C++}

1031: {\small

1032: \begin{lstlisting}[caption={Printing upper bounds for all variables using the LP solver},label=lst:lp_solver,frame=lines,float]

1033: 

1034: #include <ppl.hh>

1035: #include <iostream>

1036: 

1037: using namespace Parma_Polyhedra_Library;

1038: using namespace Parma_Polyhedra_Library::IO_Operators;

1039: 

1040: void print_upper_bounds(const C_Polyhedron& ph) {

1041:   LP_Problem lp(ph.constraints());

1042:   // Check the satisfiability of the problem.

1043:   if (!lp.is_satisfiable()) {

1044:     std::cout << "unsatisfiable" << std::endl;

1045:     return;

1046:   }

1047:   // Print the upper bound of each variable.

1048:   lp.set_optimization_mode(MAXIMIZATION);

1049:   Generator g(point());

1050:   Coefficient num, den;

1051:   const dimension_type dim = ph.space_dimension();

1052:   for (dimension_type i = 0; i < dim; ++i) {

1053:     Variable x(i);

1054:     lp.set_objective_function(x);

1055:     LP_Problem_Status status = lp.solve();

1056:     if (status == UNBOUNDED_LP_PROBLEM)

1057:       std::cout << x << " < +infty" << std::endl;

1058:     else {

1059:       assert(status == OPTIMIZED_LP_PROBLEM);

1060:       g = lp.optimizing_point();

1061:       lp.evaluate_objective_function(g, num, den);

1062:       std::cout << x << " <= " << num << "/" << den

1063:                 << std::endl;

1064:     }

1065:   }

1066: }

1067: \end{lstlisting}

1068: }

1069: 

1070: Note that the code in Listing~\ref{lst:lp_solver} is taking advantage

1071: of a limited form of incrementality provided by the LP solver: the

1072: check for satisfiability (corresponding to the first phase of the

1073: simplex algorithm) is executed only once and it is not repeated when

1074: optimizing the different objective functions (namely, only the second

1075: phase of the simplex algorithm is executed in the for-loop).  Code

1076: similar to the one above is actually used in the library itself to

1077: precisely approximate a polyhedron by means of a bounded difference or

1078: octagonal shape without incurring the potentially high cost of

1079: converting from the constraint to the generator representation of the

1080: polyhedron.

1081: 

1082: \subsection{Absence of Arbitrary Limits}

1083: 

1084: The only real restrictions imposed by the library on the client

1085: application are those caused by limitations of the available virtual

1086: memory.

1087: All data structures are fully dynamic and automatically expand

1088: (in amortized constant time) and shrink in a way that is completely

1089: transparent to the user, ensuring the best use of available memory.

1090: 

1091: In contrast, in the PolyLib, New Polka and HyTech

1092: libraries, matrices of coefficients, which are the main data

1093: structures used to represent polyhedra, cannot grow dynamically

1094: and the client application is ultimately responsible for specifying

1095: their dimensions.

1096: Since the worst case space complexity of the methods employed is

1097: exponential, in general the client application cannot make a safe and

1098: practical choice:

1099: specifying small dimensions may provoke a run-time failure;

1100: generous dimensions may waste significant amounts of memory

1101: and, again, result in unnecessary run-time failures.

1102: 

1103: \subsection{Robustness}

1104: 

1105: The clean separation between interface and implementation, among

1106: other important advantages, allows for the adoption of incremental

1107: and lazy computation techniques.

1108: The increased efficiency due to these techniques amply repays the

1109: cost of the interface checks that contribute to the library's

1110: robustness, which, as it will be explained in the sequel,

1111: is one of its most important features.

1112: 

1113: First, the library systematically checks all the interface invariants

1114: and throws an exception if any one of them is violated.

1115: This makes it very difficult to inadvertently create invalid objects

1116: and greatly simplifies the debugging of client applications.

1117: Secondly, the library is exception-safe, that is, it never leaks

1118: resources or leaves invalid object fragments around, even in the

1119: presence of exceptions.

1120: In particular, if an exception is raised, then all the memory

1121: allocated by the failed computation is discarded.

1122: These features allows applications using the PPL to use timeouts

1123: or to sensibly deal with run-time errors such as arithmetic overflows

1124: and out-of-memory conditions, so as to continue the computation in

1125: a reliable state (see below for more on this subject).

1126: %% Failure could be mitigated or even solved by suitable mechanisms for

1127: %% error detection, handling and recovery.

1128: %% This requires the ability to detect the problem,

1129: %% releasing any affected data-structure whether it be completely or

1130: %% only partially constructed,\footnote{Leaving useless data-structures around

1131: %% is a simple memory leak problem;  the presence and reachability of partially

1132: %% constructed objects is a more serious issue since it can result in

1133: %% unpredictable behavior.}

1134: %% and continue the computation.

1135: It is important to stress that, while error handling and recovery are

1136: somewhat optional features (there may be no interest in continuing the

1137: computation after an error has occurred), error detection should be

1138: considered a mandatory feature in the field of system's analysis and

1139: verification, since failure to detect an error can easily result into

1140: undefined (i.e., completely unpredictable) behavior,

1141: therefore compromising any statement about correctness.

1142: 

1143: For comparison, PolyLib detects only some errors, sometimes

1144: setting a flag and sometimes printing a message and aborting, whereas

1145: New Polka and the HyTech libraries detect some errors, print

1146: an error message and abort.  The Octagon Abstract Domain Library makes

1147: no attempt at detecting errors.  None of these libraries perform a

1148: systematic check of interface invariants.

1149: 

1150: \subsection{Resource-Bounded Computations}

1151: 

1152: The library, thanks to its exception-safety characteristics, naturally

1153: supports resource-bounded computations, that is, computations that are

1154: limited in the amount of CPU time or virtual memory or both.  The

1155: client application can take advantage of this feature by attempting a

1156: computation that is potentially very expensive imposing a maximum

1157: limit on the resources to be used.  Should this bound be exceeded, an

1158: exception is raised and the client application can resort to a

1159: simplified computation (possibly using a simpler numerical

1160: abstraction) trusting that the PPL will release all the resources

1161: allocated by the interrupted computation.  With these facilities at

1162: hand, users of the library can quite easily code resource-bounded or,

1163: at least, resource-conscious numerical abstractions.

1164: An example is shown in Listing~\ref{lst:decl-rcc}.

1165: \lstset{language=[ISO]C++}

1166: {\small

1167: \begin{lstlisting}[caption={Declaration of a class for resource-conscious computations},label=lst:decl-rcc,frame=lines,float]

1168: 

1169: #include <ppl.hh>

1170: #include <pwl.hh>

1171: #include <stdexcept>

1172: 

1173: namespace PPL = Parma_Polyhedra_Library;

1174: namespace PWL = Parma_Watchdog_Library;

1175: 

1176: class Up_Appr_Polyhedron {

1177: private:

1178:   // The type of the main polyhedral abstraction.

1179:   typedef PPL::C_Polyhedron PH;

1180: 

1181:   // The type of a simpler polyhedral abstraction.

1182:   typedef PPL::BD_Shape<mpq_class> SPH;

1183: 

1184:   PH ph;

1185: 

1186:   // Timeout in hundredth of a second; 0 for no timeout.

1187:   static unsigned long timeout_hs;

1188: 

1189:   class Timeout : public PPL::Throwable {

1190:     ...

1191:   };

1192: 

1193:   static Timeout Timeout_object;

1194: 

1195: public:

1196:   static void set_timeout(unsigned long n);

1197:   ...

1198:   void intersection_assign(const Up_Appr_Polyhedron& y);

1199:   ...

1200: };

1201: \end{lstlisting}

1202: }

1203: This uses the \emph{Parma Watchdog Library} (PWL), a library that virtualizes

1204: the interval timers for any XSI-conforming implementation of UNIX.%

1205: \footnote{XSI it is the core application

1206: programming interface for C and shell programming for systems conforming

1207: to the \emph{Single UNIX Specification}.}

1208: The PWL, which is currently distributed with the PPL, gives an

1209: application the ability to work with an unbounded number of independent

1210: ``watchdog'' timers.

1211: 

1212: The example class \verb+Up_Appr_Polyhedron+ is meant to provide

1213: convex polyhedra with ``upward approximated'', resource-conscious

1214: operations.  As the main representation it uses closed convex polyhedra;

1215: the user can set a timeout for the operations and externally impose a

1216: limit on the virtual memory available to the process.

1217: When a resource limit is reached, the class temporarily switches

1218: to a simpler family of polyhedra: bounded difference shapes.

1219: Listing~\ref{lst:def-rcc} shows a simple implementation for the intersection

1220: operation.

1221: \lstset{language=[ISO]C++}

1222: {\small

1223: \begin{lstlisting}[caption={Definition of a resource-conscious intersection method},label=lst:def-rcc,frame=lines,float]

1224: 

1225: void Up_Appr_Polyhedron

1226: ::intersection_assign(const Up_Appr_Polyhedron& y) {

1227:   if (timeout_hs == 0) {

1228:     // No timeout: do the operation directly.

1229:     ph.intersection_assign(y.ph);

1230:     return;

1231:   }

1232: 

1233:   // Save copies of `ph' and `y.ph': they may be needed

1234:   // to recover from a resources exhaustion condition.

1235:   PH xph_copy = ph;

1236:   PH yph_copy = y.ph;

1237: 

1238:   try {

1239:     PWL::Watchdog w(timeout_hs,

1240: 		    PPL::abandon_expensive_computations,

1241: 		    Timeout_object);

1242:     ph.intersection_assign(y.ph);

1243:     PPL::abandon_expensive_computations = 0;

1244:     return;

1245:   }

1246:   catch (const Timeout&) {

1247:     // Timeout expired.

1248:   }

1249:   catch (const std::bad_alloc&) {

1250:     // Out of memory.

1251:   }

1252: 

1253:   // Resources exhausted: use simpler polyhedra.

1254:   PPL::abandon_expensive_computations = 0;

1255: 

1256:   SPH xph_simple(xph_copy, PPL::POLYNOMIAL_COMPLEXITY);

1257:   SPH yph_simple(yph_copy, PPL::POLYNOMIAL_COMPLEXITY);

1258:   xph_simple.intersection_assign(yph_simple);

1259:   ph = PH(xph_simple.minimized_constraints());

1260: 

1261:   // Restore `y.ph'.

1262:   const_cast<PH&>(y.ph) = yph_copy;

1263: }

1264: \end{lstlisting}

1265: }

1266: If no timeout has been requested, then the operation is performed

1267: without any overhead.  Otherwise the polyhedra are copied, a watchdog

1268: timer, \verb+w+, is set and the operation is attempted.

1269: When \verb+w+ expires, the PPL is asked to abandon all expensive

1270: computations and to throw \verb+Timeout_object+.  Alternatively,

1271: if the process exceeds the virtual memory it has been allotted,

1272: then the \verb+bad_alloc+ standard exception will be thrown.

1273: If none of those happen, then control will be returned to the caller.

1274: Otherwise, bounded difference shapes approximating the argument

1275: polyhedra will be computed using a polynomial complexity

1276: method,%

1277: \footnote{As mentioned in Section~\ref{sec:linear-programming-problems},

1278: it is also possible to compute these approximations using a

1279: ``simplex complexity'' algorithm (i.e., theoretically exponential but

1280: very efficient in practice).}

1281: these shapes will be intersected and the intersection will be used

1282: to construct the resulting convex polyhedron.

1283: 

1284: The technique illustrated in a simplified way by Listings~\ref{lst:decl-rcc}

1285: and~\ref{lst:def-rcc} is quite powerful and allows to

1286: deal with the complexity-precision trade-off in a very flexible way.

1287: In particular, it is possible, thanks to the PWL, to work with

1288: multiple timers: while individual polyhedra operations can be guarded

1289: by a timer, other timers can monitor operations of greater

1290: granularity, such as entire analysis phases.  When an analysis phase

1291: is taking too much, then the timeouts used for the individual

1292: operations can be shortened or the analyzer can switch to a totally

1293: different, less complex analysis technique.  It is worth observing

1294: that, notwithstanding the friendliness of the PPL's user interfaces,

1295: professional applications in the field of system's analysis and

1296: verification are not expected to be directly based on the abstractions

1297: provided by the library.  Rather, the PPL abstractions have been designed

1298: so as to serve as building blocks for the actual analysis domains:

1299: in this field the complexity-precision trade-off is often so serious

1300: that the right way to face it is, by necessity, application-dependent.

1301: 

1302: \subsection{Unbounded or Native Integer Coefficients}

1303: \label{sec:unbounded-or-native-integer-coefficients}

1304: 

1305: For the representation of general convex polyhedra, with the default

1306: configuration, the Parma Polyhedra Library uses unbounded precision integers.

1307: On the other hand, if speed is important and the numerical coefficients

1308: involved are likely to be small, applications may use native integers

1309: (8, 16, 32 and 64 bit integers are supported by the PPL).

1310: This is a safe strategy since, when using native integers, the library

1311: also performs systematic (yet efficient) overflow detection.

1312: It is thus possible to adopt an approach whereby computations are first

1313: attempted with native integers.  If a computation runs to completion,

1314: the user can be certain that no overflow occurred.  Otherwise an exception

1315: is raised (as in the case seen before for resource-bounded computations),

1316: so that the client application can be restarted with bigger native

1317: integers or with unbounded integers.

1318: This is another application of the library's exception-safety, as one

1319: can rather simply code the above approach as follows:

1320: \bigskip

1321: \lstset{language=[ISO]C++}

1322: {\small

1323: \begin{lstlisting}[frame=lines]

1324: 

1325:   try {

1326:     // Analyze with 64-bit coefficients.

1327:     ...

1328:   }

1329:   catch (const std::overflow_error&) {

1330:     // Analyze with unbounded coefficients.

1331:     ...

1332:   }

1333:   ...

1334: \end{lstlisting}

1335: } % \small

1336: Again, the client application does not need to be concerned about

1337: the resources allocated by the PPL during the computation of the

1338: \verb+try+ block: everything will be deallocated automatically.

1339: 

1340: Concerning other libraries, PolyLib and New Polka can use unbounded

1341: integers as coefficients, whereas the library of HyTech does

1342: not support them.  Differently from the PPL, these libraries use

1343: finite integral types without any mechanism for overflow detection.

1344: Technically speaking and according to the C standard (the language in

1345: which they are written), this means that the effects of an overflow

1346: are completely undefined, i.e., client applications cannot make

1347: any assumption about what can happen should an overflow occur.

1348: In addition, PolyLib (and, according to \cite{BerardF99},

1349: some versions of HyTech) can use floating point values,

1350: in which case underflows and rounding errors, in addition to overflows,

1351: can affect the results.

1352: 

1353: \subsection{Portability and Documentation}

1354: 

1355: Great care has been taken to ensure the portability of the PPL.

1356: The library is written in standard \Cplusplus{}, it follows all

1357: the available applicable standards and uses sophisticated

1358: automatic configuration mechanisms.  It is known to run on all

1359: major UNIX-like operating systems, on Mac~OS~X (whether Intel-

1360: or PowerPC-based) and on Windows (via Cygwin or MinGW).

1361: 

1362: A big investment has also been made on documentation and at several

1363: levels.  First, the theoretical underpinnings have been thoroughly

1364: investigated, integrated when necessary and written down: an extensive

1365: bibliography is available on the PPL web site.  Secondly, during the

1366: entire development of the library, the quality, accessibility and

1367: completeness of the documentation has always been given a particular

1368: emphasis: while some parts of the library need more work in this respect,

1369: the vast majority of the code is thoroughly documented and some parts

1370: of it approach the ideal of ``literate programming.''

1371: 

1372: The library has been documented using the Doxygen

1373: tool.\footnote{\url{http://www.doxygen.org}.}

1374: Doxygen is a documentation system for C++, C, Java, and other languages

1375: that allows to generate high-quality documentation from a collection

1376: of documented source files.  The source files can be documented by means

1377: of ordinary comments, that can be placed near the program elements being

1378: documented: just above the declaration or definition of a member, class

1379: or namespace, for instance.  This makes it much easier to keep the

1380: documentation consistent with the actual source code.  Moreover, Doxygen

1381: allows the typesetting of mathematical formulas within comments by means

1382: of the relevant subset of \LaTeX{}, which is an important feature for

1383: a project like the PPL.  It is also able to automatically

1384: extract the code structure and use this information to generate

1385: include dependency graphs, inheritance diagrams, and collaboration diagrams.

1386: Doxygen can generate documentation in various formats, such as HTML,

1387: PostScript and PDF.  The HTML and PDF output are fully hyperlinked,

1388: a feature that greatly facilitates ``navigation'' in the available

1389: documentation.

1390: 

1391: The Parma Polyhedra Library is equipped with two manuals generated

1392: with the help of Doxygen: a user's manual, containing all and only the

1393: information needed by people wishing to use the library

1394: \cite{PPL-USER-0-9}; and a developer's reference manual that contains,

1395: in addition, all the details concerning the library implementation

1396: \cite{PPL-DEVREF-0-9}.

1397: All manuals are available, in various formats, from the PPL web site

1398: and the user's manual is also included in each source distribution.

1399: 

1400: \section{Efficiency}

1401: \label{sec:efficiency}

1402: 

1403: One natural question is how does the efficiency of the

1404: Parma Polyhedra Library compare with that of other polyhedra libraries.

1405: Of course, such a question does not have a definite answer.  Apart

1406: from clarifying whether CPU or memory efficiency or both are the

1407: intended measures of interest, the answer will depend on the targeted

1408: applications: with different applications the results can vary wildly.

1409: Moreover, even within the same application, big variations may be

1410: observed for different inputs.

1411: For these reasons, it must be admitted that the only way to meaningfully

1412: assess the performance of the library is with respect to a particular

1413: application, a particular set of problem instances, and a particular

1414: definition of `performance'.

1415: 

1416: For the same reasons, it is nonetheless instructive to compare the

1417: performance of various polyhedra libraries on a well-defined problem

1418: with a large set of freely available inputs.

1419: One such problem, called \emph{vertex/facet enumeration}, is particularly

1420: relevant for implementations based on the Double Description method

1421: such as the Parma Polyhedra Library, New Polka and PolyLib,

1422: as this problem has to be solved whenever one description has to be

1423: converted into the other one.

1424: The vertex/facet enumeration problem is a well-studied one and

1425: several systems have been expressly developed to solve it.

1426: We have thus compared the above mentioned libraries with

1427: the following (in parentheses, the versions we have tested):

1428: \begin{itemize}

1429: \item

1430: cddlib (version 0.94b), a C implementation of the Double Description

1431: method, by K.~Fukuda

1432: \cite{FukudaP96};%

1433: \footnote{\url{http://www.cs.mcgill.ca/~fukuda/soft/cdd_home/cdd.html}.}

1434: \item

1435: lrslib (version 0.42b), a C implementation of the reverse search algorithm

1436: for vertex enumeration/convex hull problems, by D.~Avis

1437: \cite{Avis98,Avis00};\footnote{\url{http://cgm.cs.mcgill.ca/~avis/C/lrs.html}.}

1438: \item

1439: pd (version 1.7), a C program implementing a primal-dual algorithm

1440: using rational arithmetic, by A.~Marzetta and maintained by D.~Bremner

1441: \cite{BremnerFM98}.%

1442: \footnote{\url{http://www.cs.unb.ca/profs/bremner/pd/}.}

1443: \end{itemize}

1444: Both cddlib and lrslib come with driver programs that support a polyhedra

1445: input format that was introduced by K.~Fukuda and extended by D.~Avis;

1446: this input format is also supported by the pd program.

1447: The distributions of cddlib and lrslib provide more than 100 different inputs

1448: of varying complexity for these programs.

1449: Driver programs that can read the same input format and use the PPL,

1450: New Polka and PolyLib are part of the PPL distribution since version 0.7.

1451: 

1452: The tests have been performed on a PC equipped with an AMD Athlon 2800+

1453: with 1 GB of RAM and running GNU/Linux and GMP version 4.2.

1454: All the software has been compiled with GCC 4.0.3 at the optimization level

1455: that is the default for each package (i.e., the PPL was compiled with

1456: `\verb/-O2/', its default; PolyLib, cddlib, and pd with \verb/-O2/;

1457: New Polka and lrslib with `\verb/-O3/').

1458: The obtained running times, in seconds, are reported

1459: in Tables~\ref{tab:efficiency-vertex-enumeration}

1460: and~\ref{tab:efficiency-vertex-enumeration-hard}.%

1461: \footnote{Filenames have been shortened to fit the table on the page:

1462: in particular the \texttt{.ext} and \texttt{.ine} extensions have been

1463: shortened to \texttt{.e} and \texttt{.i}, respectively; moreover, the file

1464: called \texttt{integralpoints.ine} has been renamed \texttt{integpoints.i}.}

1465: The entries marked with `n.a.' in the pd's column indicate the problems

1466: that cannot be solved by pd, which can only handle polyhedra that contain

1467: the origin.  Entries marked with `ovfl' indicate the problems on which

1468: pd runs into an arithmetic overflow.

1469: It should be noted that strictly speaking, lrslib solves a slightly

1470: different, easier problem than the one solved by the other systems:

1471: while the latter guarantee the result is minimized, the output of

1472: lrslib may contain duplicate rays.

1473: 

1474: {

1475: \renewcommand{\arraystretch}{0.91}

1476: \small

1477: \begin{longtable}{l......}

1478: \caption{Efficiency on vertex enumeration%

1479: \label{tab:efficiency-vertex-enumeration}} \\

1480: \hline

1481: \multicolumn{1}{c}{input} &

1482: \multicolumn{1}{c}{PPL} &

1483: \multicolumn{1}{c}{New Polka} &

1484: \multicolumn{1}{c}{PolyLib} &

1485: \multicolumn{1}{c}{cddlib} &

1486: \multicolumn{1}{c}{lrslib} &

1487: \multicolumn{1}{c}{pd} \\

1488: \hline

1489: \endfirsthead

1490: \caption[]{Efficiency on vertex enumeration (continued)} \\

1491: \hline

1492: \multicolumn{1}{c}{input} &

1493: \multicolumn{1}{c}{PPL} &

1494: \multicolumn{1}{c}{New Polka} &

1495: \multicolumn{1}{c}{PolyLib} &

1496: \multicolumn{1}{c}{cddlib} &

1497: \multicolumn{1}{c}{lrslib} &

1498: \multicolumn{1}{c}{pd} \\

1499: \hline

1500: \endhead

1501: \hline

1502: \endfoot

1503: \verb/ccc4.e/&0.00&0.11&0.03&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1504: \verb/ccc5.e/&0.00&0.10&0.04&0.02&0.00&\multicolumn{1}{c}{n.a.}\\

1505: \verb/ccc6.e/&0.03&0.14&0.26&0.61&3.12&\multicolumn{1}{c}{n.a.}\\

1506: \verb/ccp4.e/&0.00&0.10&0.02&0.00&0.00&0.01 \\

1507: \verb/ccp5.e/&0.00&0.10&0.04&0.02&0.00&5.36 \\

1508: \verb/ccp6.e/&0.05&0.15&0.31&0.90&3.95&\multicolumn{1}{c}{$>1h$} \\

1509: \verb/cp4.e/&0.00&0.08&0.03&0.00&0.00&0.01 \\

1510: \verb/cp5.e/&0.00&0.12&0.05&0.02&0.00&5.29 \\

1511: \verb/cp6.e/&0.05&0.18&0.30&0.88&3.86&\multicolumn{1}{c}{$>1h$} \\

1512: \verb/cube.e/&0.00&0.05&0.02&0.00&0.00&0.00 \\

1513: \verb/cut16_11.e/&0.00&0.12&0.04&0.02&0.00&3.86 \\

1514: \verb/cut32_16.e/&0.05&0.17&0.28&0.91&4.32&\multicolumn{1}{c}{$>1h$} \\

1515: \verb/cyclic10-4.e/&0.00&0.07&0.02&0.00&0.00&0.00 \\

1516: \verb/cyclic12-6.e/&0.00&0.08&0.03&0.01&0.00&0.44 \\

1517: \verb/cyclic14-8.e/&0.00&0.09&0.04&0.06&0.01&172.10 \\

1518: \verb/cyclic16-10.e/&0.02&0.14&0.07&0.24&0.04&\multicolumn{1}{c}{$>1h$} \\

1519: \verb/dcube10.e/&0.02&0.13&0.10&0.23&0.02&\multicolumn{1}{c}{$>1h$} \\

1520: \verb/dcube12.e/&0.17&0.22&2.66&1.29&0.10&\multicolumn{1}{c}{$>1h$} \\

1521: \verb/dcube3.e/&0.00&0.08&0.02&0.00&0.00&0.00 \\

1522: \verb/dcube6.e/&0.00&0.07&0.03&0.00&0.00&0.35 \\

1523: \verb/dcube8.e/&0.00&0.12&0.03&0.04&0.00&119.53 \\

1524: \verb/irbox20-4.e/&0.00&0.08&0.01&0.01&0.00&0.01 \\

1525: \verb/irbox200-4.e/&0.02&0.07&0.02&0.98&0.05&0.18 \\

1526: \verb/mp5.e/&0.00&0.11&0.05&0.59&0.84&3.93 \\

1527: \verb/prodst62.e/&34.78&161.09&123.28&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{ovfl} \\

1528: \verb/redcheck.e/&0.00&0.06&0.01&0.00&0.00&0.00 \\

1529: \verb/reg24-5.e/&0.00&0.08&0.03&0.01&0.00&0.01 \\

1530: \verb/reg600-5_m.e/&5.05&19.12&12.37&135.49&33.63&\multicolumn{1}{c}{n.a.}\\

1531: \verb/samplev1.e/&0.00&0.09&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1532: \verb/samplev2.e/&0.00&0.06&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1533: \verb/samplev3.e/&0.00&0.07&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1534: \verb/tsp5.e/&0.00&0.12&0.04&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1535: %\verb/1d.i/&0.00&0.08&0.01&0.00&\textit{0}.\textit{00}&\multicolumn{1}{c}{n.a.}\\

1536: %\verb/1da.i/&0.00&0.07&0.01&0.00&\textit{0}.\textit{00}&\multicolumn{1}{c}{n.a.}\\

1537: \verb/allzero.i/&0.00&0.06&0.01&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1538: \verb/cp4.i/&0.00&0.09&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1539: \verb/cp5.i/&0.01&0.12&0.05&0.14&5.91&\multicolumn{1}{c}{n.a.}\\

1540: \verb/cross10.i/&0.08&0.22&0.14&10.50&\multicolumn{1}{c}{$>1h$}&1.38 \\

1541: \verb/cross12.i/&0.84&3.04&2.86&166.15&\multicolumn{1}{c}{$>1h$}&15.24 \\

1542: \verb/cross4.i/&0.00&0.07&0.02&0.00&0.00&0.00 \\

1543: \verb/cross6.i/&0.00&0.06&0.03&0.04&0.09&0.01 \\

1544: \verb/cross8.i/&0.01&0.07&0.03&0.54&28.90&0.14 \\

1545: \verb/cube.i/&0.00&0.09&0.02&0.00&0.00&0.00 \\

1546: \verb/cube10.i/&0.02&0.15&0.16&0.24&0.03&\multicolumn{1}{c}{$>1h$} \\

1547: \verb/cube12.i/&0.19&0.32&3.70&1.35&0.18&\multicolumn{1}{c}{$>1h$} \\

1548: \verb/cube3.i/&0.00&0.06&0.02&0.00&0.00&0.00 \\

1549: \verb/cube6.i/&0.00&0.10&0.03&0.01&0.00&0.34 \\

1550: \verb/cube8.i/&0.00&0.10&0.05&0.06&0.00&123.23 \\

1551: \verb/cubetop.i/&0.00&0.08&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1552: \verb/cubocta.i/&0.00&0.10&0.02&0.00&0.00&0.00 \\

1553: \verb/cyc.i/&0.00&0.08&0.01&0.00&0.00&0.00 \\

1554: \verb/cyclic17_8.i/&0.04&0.15&0.14&0.32&0.08&\multicolumn{1}{c}{$>1h$} \\

1555: \verb/diamond.i/&0.00&0.08&0.01&0.00&0.00&0.00 \\

1556: \verb/dodeca_m.i/&0.00&0.07&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1557: \verb/ex1.i/&0.00&0.07&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1558: \verb/grcubocta.i/&0.00&0.06&0.02&0.01&0.00&0.01 \\

1559: \verb/hexocta.i/&0.00&0.05&0.01&0.02&0.00&0.01 \\

1560: \verb/icododeca_m.i/&0.00&0.07&0.02&0.05&0.00&\multicolumn{1}{c}{n.a.}\\

1561: \verb/in0.i/&0.00&0.06&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1562: \verb/in1.i/&0.00&0.08&0.02&0.01&0.00&\multicolumn{1}{c}{n.a.}\\

1563: \verb/in2.i/&0.00&0.08&0.03&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1564: \verb/in3.i/&0.00&0.05&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1565: \verb/in4.i/&0.00&0.10&0.03&0.01&0.00&\multicolumn{1}{c}{n.a.}\\

1566: \verb/in5.i/&0.00&0.07&0.04&0.03&0.00&\multicolumn{1}{c}{n.a.}\\

1567: \verb/in6.i/&0.02&0.14&0.09&0.42&0.03&\multicolumn{1}{c}{n.a.}\\

1568: \verb/in7.i/&0.18&0.40&0.44&0.96&0.08&\multicolumn{1}{c}{n.a.}\\

1569: \verb/infeas.i/&0.00&0.09&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1570: \verb/integpoints.i/&0.00&0.10&0.04&0.05&0.00&\multicolumn{1}{c}{n.a.}\\

1571: \verb/kkd18_4.i/&0.00&0.10&0.02&0.02&0.00&\multicolumn{1}{c}{n.a.}\\

1572: \verb/kkd27_5.i/&0.05&0.12&0.07&0.08&0.01&\multicolumn{1}{c}{n.a.}\\

1573: \verb/kkd38_6.i/&2.95&5.26&1.52&0.32&0.05&\multicolumn{1}{c}{n.a.}\\

1574: \verb/kq20_11_m.i/&0.19&0.41&0.45&0.99&0.08&\multicolumn{1}{c}{n.a.}\\

1575: \verb/metric40_11.i/&0.00&0.11&0.04&0.07&0.57&\multicolumn{1}{c}{n.a.}\\

1576: \verb/metric80_16.i/&0.13&0.24&0.07&0.54&32.09&\multicolumn{1}{c}{n.a.}\\

1577: \verb/mit31-20.i/&23.34&27.21&115.00&103.19&25.53&\multicolumn{1}{c}{$>1h$} \\

1578: \verb/mp5.i/&0.00&0.08&0.04&0.06&0.58&\multicolumn{1}{c}{n.a.}\\

1579: \verb/mp5a.i/&0.00&0.10&0.03&0.06&0.57&\multicolumn{1}{c}{n.a.}\\

1580: \verb/mp6.i/&0.33&0.42&0.75&4.66&1177.96&\multicolumn{1}{c}{n.a.}\\

1581: \verb/nonfull.i/&0.00&0.06&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1582: \verb/origin.i/&0.00&0.08&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1583: \verb/project1_m.i/&0.00&0.10&0.04&0.03&0.00&1.10 \\

1584: \verb/project1res.i/&0.00&0.08&0.02&0.00&0.00&0.00 \\

1585: \verb/project2_m.i/&0.02&0.09&0.05&0.46&0.13&\multicolumn{1}{c}{n.a.}\\

1586: \verb/project2res.i/&0.00&0.08&0.02&0.08&0.01&\multicolumn{1}{c}{n.a.}\\

1587: \verb/rcubocta.i/&0.00&0.08&0.01&0.01&0.00&0.01 \\

1588: \verb/reg24-5.i/&0.00&0.08&0.02&0.01&0.00&0.01 \\

1589: \verb/rhomtria_m.i/&0.00&0.09&0.02&0.04&0.00&\multicolumn{1}{c}{n.a.}\\

1590: \verb/sample.i/&0.00&0.08&0.01&0.00&0.00&0.00 \\

1591: \verb/sampleh1.i/&0.00&0.05&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1592: \verb/sampleh2.i/&0.00&0.06&0.01&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1593: \verb/sampleh3.i/&0.00&0.04&0.02&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1594: \verb/sampleh4.i/&0.00&0.07&0.01&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1595: \verb/sampleh5.i/&0.00&0.05&0.01&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1596: \verb/sampleh6.i/&0.00&0.06&0.01&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1597: \verb/sampleh7.i/&0.00&0.09&0.01&0.00&0.00&\multicolumn{1}{c}{n.a.}\\

1598: \verb/sampleh8.i/&52.87&73.64&78.76&\multicolumn{1}{c}{$>1h$}&4.59&\multicolumn{1}{c}{n.a.}\\

1599: \verb/trunc10.i/&8.81&9.06&0.08&1.66&9.15&737.37 \\

1600: \verb/trunc7.i/&0.02&0.13&0.04&0.13&0.16&17.51 \\

1601: \verb/tsp5.i/&0.00&0.10&0.04&0.02&0.00&\multicolumn{1}{c}{n.a.}\\

1602: \hline

1603: total&130.34&308.12&345.70

1604: \end{longtable}

1605: } % \small

1606: 

1607: In Table~\ref{tab:efficiency-vertex-enumeration-hard} we have collected

1608: the data concerning the hardest of these problems.  Here we have imposed

1609: a memory limit of 768~MB: entries marked with `mem' indicate the problems

1610: on which this limit was exceeded.

1611: The entries marked with `tab' in the New Polka's column indicate the problems

1612: where New Polka ran ``out of table space'' in the conversion algorithm.

1613: 

1614: {

1615: \renewcommand{\arraystretch}{0.91}

1616: \small

1617: \begin{longtable}{l......}

1618: \caption{Efficiency on vertex enumeration: hard problems%

1619: \label{tab:efficiency-vertex-enumeration-hard}} \\

1620: \hline

1621: \multicolumn{1}{c}{input} &

1622: \multicolumn{1}{c}{PPL} &

1623: \multicolumn{1}{c}{New Polka} &

1624: \multicolumn{1}{c}{PolyLib} &

1625: \multicolumn{1}{c}{cddlib} &

1626: \multicolumn{1}{c}{lrslib} &

1627: \multicolumn{1}{c}{pd} \\

1628: \hline

1629: \endhead

1630: \hline

1631: \endfoot

1632: \verb/cp7.e/&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{tab}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{$>1h$} \\

1633: \verb/cyclic25_13.e/&89.94&\multicolumn{1}{c}{tab}&354.83&221.98&12.10&\multicolumn{1}{c}{n.a.}\\

1634: \verb/cp6.i/&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{tab}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{n.a.}\\

1635: \verb/mit.i/&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{tab}&\multicolumn{1}{c}{$>1h$}&950.00&2024.16&\multicolumn{1}{c}{n.a.}\\

1636: \verb/mit288-281.i/&\multicolumn{1}{c}{mem}&\multicolumn{1}{c}{tab}&\multicolumn{1}{c}{mem}&\multicolumn{1}{c}{mem}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{ovfl} \\

1637: \verb/mit41-16.i/&137.14&\multicolumn{1}{c}{tab}&320.37&325.65&33.89&\multicolumn{1}{c}{$>1h$} \\

1638: \verb/mit708-9.i/&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{tab}&\multicolumn{1}{c}{$>1h$}&1016.23&1927.18&\multicolumn{1}{c}{n.a.}\\

1639: \verb/mit71-61.i/&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{tab}&\multicolumn{1}{c}{mem}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{n.a.}\\

1640: \verb/mit90-86.i/&\multicolumn{1}{c}{mem}&\multicolumn{1}{c}{tab}&\multicolumn{1}{c}{mem}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{$>1h$}&\multicolumn{1}{c}{ovfl} \\

1641: \end{longtable}

1642: } % \small

1643: 

1644: Another possibility of evaluating the performance of the Parma Polyhedra

1645: Library on a standard problem with standard data is offered by linear

1646: programming, which is the paradigm upon which several approaches

1647: to analysis and verification

1648: (such as, e.g., \cite{SankaranarayananCSM06,SankaranarayananSM05})

1649: rest upon.  This requires either a version of the simplex based on

1650: exact arithmetic, or, in case a classical floating-point

1651: implementation is used, it forces to validate the obtained result

1652: with some alternative methods.

1653: The \emph{MathSAT}\footnote{\url{http://mathsat.itc.it/}.} decision procedure

1654: \cite{BozzanoBCJRSS05},

1655: which is applicable to the formal verification of infinite state systems

1656: (such as timed and hybrid systems), is based on a version of

1657: the \emph{Cassowary Constraint Solving Toolkit} \cite{BadrosBS01},

1658: modified so as to use

1659: exact arithmetic instead of floating-point numbers.

1660: Moreover, the algorithm employed by MathSAT requires incremental

1661: satisfiability checks: a set of constraints is added and satisfiability

1662: is checked, more constraints are added and satisfiability is re-checked,

1663: and so forth.

1664: We have thus measured the efficiency of the PPL's incremental constraint

1665: solver by comparison with the version of Cassowary used in MathSAT and with

1666: the \emph{Wallaroo Linear Constraint Solving

1667: Library},\footnote{\url{http://sourceforge.net/projects/wallaroo/}.}

1668: another descendant of Cassowary.

1669: The benchmarks we used are quite standard in the linear programming community:

1670: they come from the `\verb+lp+' directory of

1671: \emph{NetLib}.\footnote{\url{http://www.netlib.org/lp/index.html}.}

1672: The solution times, in seconds, obtained for the problem of adding one

1673: constraint at a time, checking for satisfiability at each step, are given in

1674: Table~\ref{tab:efficiency-simplex-incremental-satisfiability}.

1675: 

1676: {

1677: \renewcommand{\arraystretch}{0.91}

1678: \small

1679: \begin{longtable}{l......}

1680: \caption{Efficiency of the simplex solver on incremental satisfiability checking%

1681: \label{tab:efficiency-simplex-incremental-satisfiability}} \\

1682: \hline

1683: \multicolumn{1}{c}{input} &

1684: \multicolumn{1}{c}{PPL} &

1685: \multicolumn{1}{c}{Wallaroo} &

1686: \multicolumn{1}{c}{Cassowary/MathSAT} \\

1687: \hline

1688: \endhead

1689: \hline

1690: \endfoot

1691: \verb/adlittle.mps/ &  0.33 &  1.46 &  1.51 \\

1692: \verb/afiro.mps/    &  0.02 &  0.05 &  0.07 \\

1693: \verb/blend.mps/    & 13.45 &  5.40 &  8.23 \\

1694: \verb/boeing1.mps/  & 47.28 & 87.80 & 75.48 \\

1695: \verb/boeing2.mps/  &  2.32 & 10.58 & 14.67 \\

1696: \verb/kb2.mps/      &  0.11 &  0.30 &  0.46 \\

1697: \verb/sc105.mps/    &  0.48 & 10.95 &  7.23 \\

1698: \verb/sc50a.mps/    &  0.05 &  0.64 &  0.56 \\

1699: \verb/sc50b.mps/    &  0.06 &  0.70 &  0.94\\

1700: \hline

1701: total                & 64.10 &117.88 &109.15

1702: \end{longtable}

1703: } % \small

1704: 

1705: \section{Development Plans}

1706: \label{sec:development-plans}

1707: 

1708: In this section we briefly review the short- and mid-term development

1709: plans we have for the library.  We deliberately omit all long-term

1710: projects: for all those we mention here, code ---whether in the form of a

1711: prototype or as a proof-of-concept exercise--- has already been developed

1712: that proves the feasibility of the proposal.

1713: 

1714: \subsection{More Abstractions}

1715: 

1716: \paragraph*{Intervals and Bounding Boxes}

1717: An important numerical domain is the domain of \emph{bounding boxes}:

1718: these are representable by means of finite set of \emph{intervals} or

1719: be seen as finite conjunctions of constraints of the form $\pm v_i \leq d$

1720: or $\pm v_i < d$.  Despite the fact that bounding boxes have been one of

1721: the first abstract domains ever proposed \cite{CousotC76} and that they

1722: have been implemented and reimplemented dozens of times, no freely available

1723: implementation is really suitable for the purposes of abstract interpretation.

1724: In fact, the available interval libraries either lack support

1725: for non-closed intervals (so that they are unable to represent

1726: constraints of the form $\pm v_i < d$), or they do not provide the right

1727: support for approximation in the sense of partial correctness

1728: (e.g., division by an interval containing zero gives rise to a run-time error

1729: instead of giving an interval containing the result under the assumption

1730: that the concrete division being approximated was not a division by zero), or

1731: they disregard rounding errors and are therefore unsafe.

1732: %

1733: We are thus working at a complete implementation of bounding boxes based

1734: on intervals. Such intervals are parametric on a number of features:

1735: they support open as well as closed boundaries;

1736: boundaries can be chosen within one of the number families mentioned

1737: in Section~\ref{sec:bounded-difference-shapes} (when boundaries are floating

1738: point numbers, rounding is of course controlled to maintain soundness);

1739: independently from the type of the boundaries, both plain intervals of real

1740: numbers and intervals subject to generic \emph{restrictions} are supported.

1741: This notion of restriction can be instantiated to obtain intervals of integer

1742: numbers, \emph{modulo intervals} \cite{NakanishiF01,NakanishiJPF99},

1743: and generalizations of the latter providing more precise

1744: information.\footnote{An implementation of these interval families

1745: is already available in the PPL's public CVS repository.}

1746: 

1747: \paragraph*{Grid-Polyhedra}

1748: An interesting line of development consists in the combination of the grids

1749: domain with the several polyhedral domains provided by the PPL:

1750: not only the $\mathbb{Z}$-polyhedra domain \cite{Ancourt91th},

1751: but also many variations such as grid-polyhedra, grid-octagon,

1752: grid-bounded-difference, grid-interval domains

1753: (not to mention their powersets).

1754: 

1755: \paragraph*{Polynomial Equalities and Inequalities}

1756: The work in \cite{BagnaraR-CZ05} proved the feasibility of representing

1757: systems of polynomial inequalities of bounded degree by encoding them

1758: into convex polyhedra.  The prototype implementation used for the

1759: experimental evaluation presented in \cite{BagnaraR-CZ05} is being

1760: turned into a complete abstract domain and will be incorporated into

1761: the PPL.

1762: 

1763: \subsection{More Language Interfaces}

1764: 

1765: The current version of the PPL only offers C and Prolog interfaces for

1766: (C and NNC) polyhedra and LP problems.  It would not be difficult to

1767: add, along the same lines, interfaces for all the other abstractions.

1768: It can be done, rather quickly, mostly as a ``copy and paste'' exercise.

1769: Instead of following that route (which would imply substantial code

1770: duplication and an unaffordable maintenance burden), we are working

1771: at an automatic way of obtaining these interfaces out of a few ``templates.''

1772: As part of this ongoing effort, we are extending the set of available

1773: \emph{direct} interfaces\footnote{As opposed to the \emph{indirect}

1774: interfaces that can be obtained by passing through the C interface.}

1775: with Java and Objective Caml.\footnote{Initial versions of these interfaces

1776: are already available in the PPL's public CVS repository.}

1777: Finally there are plans to develop an interface that allows

1778: to use the PPL's numerical abstractions within

1779: \emph{Mathematica}.\footnote{\url{http://www.wolfram.com/}.}

1780: 

1781: \subsection{Other Features}

1782: 

1783: Other features on the horizon of the Parma Polyhedra Library include

1784: the inclusion of:

1785: bidirectional serialization functions for all the supported abstractions;

1786: the ask-and-tell generic construction of \cite{Bagnara97th};%

1787: \footnote{Preliminary support for both these features is already available

1788: in the PPL's public CVS repository.}

1789: and the extrapolation operators defined in \cite{HenzingerH95}

1790: and \cite{HenzingerPW01};

1791: We also plan to add support for more complexity-throttling techniques

1792: such as:

1793: breaking down the set of the variables of interests into ``packs''

1794: of manageable size \cite{BlanchetCCFMMMR03,CousotCFMMMR05,VenetB04};

1795: support for Cartesian factoring as defined in \cite{HalbwachsMP-V03};

1796: and the limitation of the number of constraints and generators

1797: and/or the size of coefficients in the representation

1798: of polyhedra \cite{Frehse05}.

1799: 

1800: \section{Discussion}

1801: \label{sec:discussion}

1802: 

1803: In this paper, we have presented the Parma Polyhedra Library, a library

1804: of numerical abstractions especially targeted to applications in the

1805: field of analysis and verification of software and hardware systems.

1806: We have illustrated the general philosophy that is behind the design

1807: of the library, its main features, examples highlighting the advantages

1808: offered to client applications, and the avenue we have prepared for

1809: future developments.

1810: 

1811: The Parma Polyhedra Library is being used on several applications

1812: in the field of verification of hardware and software systems.

1813: It has been used for the verification of properties of oscillator circuits

1814: \cite{FrehseKR06,FrehseKRM05};

1815: to verify the soundness of \emph{batch workflow networks}

1816: (a kind of Petri nets used in workflow management) \cite{vanHeeOSV06};

1817: in the field of safety analysis of continuous and hybrid systems

1818: to overapproximate the systems of linear differential equations

1819: expressing the dynamics of hybrid automata

1820: \cite{DoyenHR05,Frehse04,FrehseHK04,SankaranarayananSM06} and,

1821: in particular, the PPL is used in PHAVer, an innovative tool for the

1822: verification of such systems \cite{Frehse05}.

1823: The PPL is also used: in a version of \emph{TVLA} (3-Valued Logic Analysis

1824: Engine, \url{http://www.cs.tau.ac.il/~tvla/}), a system for the verification

1825: of properties of arrays and heap-allocated data \cite{GopanRS05};

1826: in \emph{iCSSV} (interprocedural C String Static

1827: Verifier), a tool for verifying the safety of string operations in C programs

1828: \cite{Ellenbogen04th};

1829: and in a static analyzer

1830: for \emph{gated data dependence graphs}, an intermediate representation

1831: for optimizing compilation \cite{HymansU04}.  This analyzer employs,

1832: in particular, the precise widening operator and the widening with tokens

1833: technique introduced in \cite{BagnaraHRZ03,BagnaraHRZ05SCP}.

1834: In \cite{SankaranarayananCSM06} the PPL is used to derive invariant linear

1835: equalities and inequalities for a subset of the C language;

1836: it is used in \emph{StInG} \cite{SankaranarayananSM04} and \emph{LPInv}

1837: \cite{SankaranarayananSM05}, two systems for the analysis of transition

1838: systems;

1839: it is used for the model-checking of reconfigurable hybrid

1840: systems \cite{SongCR05};

1841: it is used in a static analysis tool for x86 binaries

1842: that automatically identifies instructions

1843: that can be used to redirect control flow, thus constituting

1844: vulnerabilities that can be exploited in order to bypass

1845: intrusion detection systems \cite{KruegelKMRV05};

1846: it is also used to represent and validate real-time systems' constraints

1847: and behaviors \cite{DooseM05}

1848: and to automatically derive the \emph{argument size relations}

1849: that are needed for termination analysis of Prolog programs

1850: \cite{MesnardB05TPLP}.

1851: 

1852: In conclusion, even though the library is still not mature and

1853: functionally complete, it already offers a combination of

1854: functionality, reliability, usability and performance that is not

1855: matched by similar, freely available libraries.  Moreover, since the

1856: PPL is free software and distributed under the terms of the GNU

1857: General Public License (GPL), and due to the presence of extensive

1858: documentation, the library can already be regarded as an important

1859: contribution secured to the community.

1860: 

1861: For the most up-to-date information, documentation and downloads

1862: and to follow the development work, the reader is referred to the

1863: Parma Polyhedra Library site at \url{http://www.cs.unipr.it/ppl/}.

1864: 

1865: 

1866: \bigskip

1867: \noindent

1868: {\bfseries Acknowledgments.}

1869: We would like to express our gratitude and appreciation to all the

1870: present and past developers of the Parma Polyhedra Library:

1871: \italian{Irene Bacchi},

1872: \italian{Abramo Bagnara},

1873: \italian{Danilo Bonardi},

1874: \italian{Sara Bonini},

1875: \italian{Andrea Cimino},

1876: Katy Dobson,

1877: \italian{Giordano Fracasso},

1878: \italian{Maximiliano Marchesi},

1879: \italian{Elena Mazzi},

1880: David Merchat,

1881: Matthew Mundell,

1882: \italian{Andrea Pescetti},

1883: \italian{Barbara Quartieri},

1884: \italian{Elisa Ricci},

1885: Enric Rodr\'\i guez-Carbonell,

1886: \italian{Angela Stazzone},

1887: \italian{Fabio Trabucchi},

1888: \italian{Claudio Trento},

1889: \italian{Alessandro Zaccagnini},

1890: \italian{Tatiana Zolo}.

1891: Thanks also

1892: to Aaron Bradley, for contributing to the project his

1893: \emph{Mathematica} interface,

1894: to Goran Frehse, for contributing his code to limit the complexity

1895: of polyhedra,

1896: and to all the users of the library that provided us with

1897: helpful feedback.

1898: 

1899: %\bibliographystyle{elsart-num}

1900: %\bibliographystyle{plain}

1901: %\bibliography{ppl,ppl_citations,mybib}

1902: 

1903: \newcommand{\noopsort}[1]{}\hyphenation{ Ba-gna-ra Bie-li-ko-va Bruy-noo-ghe

1904:   Common-Loops DeMich-iel Dober-kat Di-par-ti-men-to Er-vier Fa-la-schi

1905:   Fell-eisen Gam-ma Gem-Stone Glan-ville Gold-in Goos-sens Graph-Trace

1906:   Grim-shaw Her-men-e-gil-do Hoeks-ma Hor-o-witz Kam-i-ko Kenn-e-dy Kess-ler

1907:   Lisp-edit Lu-ba-chev-sky Ma-te-ma-ti-ca Nich-o-las Obern-dorf Ohsen-doth

1908:   Par-log Para-sight Pega-Sys Pren-tice Pu-ru-sho-tha-man Ra-guid-eau Rich-ard

1909:   Roe-ver Ros-en-krantz Ru-dolph SIG-OA SIG-PLAN SIG-SOFT SMALL-TALK Schee-vel

1910:   Schlotz-hauer Schwartz-bach Sieg-fried Small-talk Spring-er Stroh-meier

1911:   Thing-Lab Zhong-xiu Zac-ca-gni-ni Zaf-fa-nel-la Zo-lo }

1912: \begin{thebibliography}{10}

1913: 

1914: \bibitem{AllenK85}

1915: J.~F. Allen and H.~A. Kautz.

1916: \newblock A model of naive temporal reasoning.

1917: \newblock In J.~R. Hobbs and R.~Moore, editors, {\em Formal Theories of the

1918:   Commonsense World}, pages 251--268. Ablex, Norwood, NJ, 1985.

1919: 

1920: \bibitem{Ancourt91th}

1921: C.~Ancourt.

1922: \newblock {\em G\'en\'eration automatique de codes de transfert pour

1923:   multiprocesseurs \`a m\'emoires locales}.

1924: \newblock PhD thesis, Universit\'e de Paris VI, Paris, France, March 1991.

1925: 

1926: \bibitem{Avis98}

1927: D.~Avis.

1928: \newblock Computational experience with the reverse search vertex enumeration

1929:   algorithm.

1930: \newblock {\em Optimization Methods and Software}, 10:107--124, 1998.

1931: 

1932: \bibitem{Avis00}

1933: D.~Avis.

1934: \newblock {lrs}: A revised implementation of the reverse search vertex

1935:   enumeration algorithm.

1936: \newblock In G.~Kalai and G.~M. Ziegler, editors, {\em Polytopes ---

1937:   Combinatorics and Computation}, volume~29 of {\em Oberwolfach Seminars},

1938:   pages 177--198. {Birkh\"auser-Verlag}, 2000.

1939: 

1940: \bibitem{BadrosBS01}

1941: G.~J. Badros, A.~Borning, and P.~J. Stuckey.

1942: \newblock The {Cassowary} linear arithmetic constraint solving algorithm.

1943: \newblock {\em ACM Transactions on Computer-Human Interaction}, 8(4):267--306,

1944:   2001.

1945: 

1946: \bibitem{Bagnara97th}

1947: R.~Bagnara.

1948: \newblock {\em Data-Flow Analysis for Constraint Logic-Based Languages}.

1949: \newblock PhD thesis, Dipartimento di Informatica, Universit\`a di Pisa, Pisa,

1950:   Italy, March 1997.

1951: \newblock Printed as Report TD-1/97.

1952: 

1953: \bibitem{Bagnara98SCP}

1954: R.~Bagnara.

1955: \newblock A hierarchy of constraint systems for data-flow analysis of

1956:   constraint logic-based languages.

1957: \newblock {\em Science of Computer Programming}, 30(1--2):119--155, 1998.

1958: 

1959: \bibitem{BagnaraDHMZ06a}

1960: R.~Bagnara, K.~Dobson, P.~M. Hill, M.~Mundell, and E.~Zaffanella.

1961: \newblock Grids: A domain for analyzing the distribution of numerical values,

1962:   2006.

1963: \newblock Accepted for publication and presented at the International Symposium

1964:   on Logic-based Program Synthesis and Transformation.

1965: 

1966: \bibitem{BagnaraDHMZ06b}

1967: R.~Bagnara, K.~Dobson, P.~M. Hill, M.~Mundell, and E.~Zaffanella.

1968: \newblock A practical tool for analyzing the distribution of numerical values,

1969:   2006.

1970: \newblock Submitted for publication. Available at

1971:   \url{http://www.comp.leeds.ac.uk/hill/Papers/papers.html}.

1972: 

1973: \bibitem{BagnaraHMZ05}

1974: R.~Bagnara, P.~M. Hill, E.~Mazzi, and E.~Zaffanella.

1975: \newblock Widening operators for weakly-relational numeric abstractions.

1976: \newblock In C.~Hankin and I.~Siveroni, editors, {\em Static Analysis:

1977:   Proceedings of the 12th International Symposium}, volume 3672 of {\em Lecture

1978:   Notes in Computer Science}, pages 3--18, London, UK, 2005. Springer-Verlag,

1979:   Berlin.

1980: 

1981: \bibitem{BagnaraHRZ03}

1982: R.~Bagnara, P.~M. Hill, E.~Ricci, and E.~Zaffanella.

1983: \newblock Precise widening operators for convex polyhedra.

1984: \newblock In R.~Cousot, editor, {\em Static Analysis: Proceedings of the 10th

1985:   International Symposium}, volume 2694 of {\em Lecture Notes in Computer

1986:   Science}, pages 337--354, San Diego, California, USA, 2003. Springer-Verlag,

1987:   Berlin.

1988: 

1989: \bibitem{BagnaraHRZ05SCP}

1990: R.~Bagnara, P.~M. Hill, E.~Ricci, and E.~Zaffanella.

1991: \newblock Precise widening operators for convex polyhedra.

1992: \newblock {\em Science of Computer Programming}, 58(1--2):28--56, 2005.

1993: 

1994: \bibitem{BagnaraHZ05FAC}

1995: R.~Bagnara, P.~M. Hill, and E.~Zaffanella.

1996: \newblock Not necessarily closed convex polyhedra and the double description

1997:   method.

1998: \newblock {\em Formal Aspects of Computing}, 17(2):222--257, 2005.

1999: 

2000: \bibitem{PPL-DEVREF-0-9}

2001: R.~Bagnara, P.~M. Hill, and E.~Zaffanella.

2002: \newblock {\em The {Parma Polyhedra Library} Developer's Manual}.

2003: \newblock Department of Mathematics, University of Parma, Parma, Italy, release

2004:   0.9 edition, March 2006.

2005: \newblock Available at \url{http://www.cs.unipr.it/ppl/}.

2006: 

2007: \bibitem{PPL-USER-0-9}

2008: R.~Bagnara, P.~M. Hill, and E.~Zaffanella.

2009: \newblock {\em The {Parma Polyhedra Library} User's Manual}.

2010: \newblock Department of Mathematics, University of Parma, Parma, Italy, release

2011:   0.9 edition, March 2006.

2012: \newblock Available at \url{http://www.cs.unipr.it/ppl/}.

2013: 

2014: \bibitem{BagnaraHZ06STTT}

2015: R.~Bagnara, P.~M. Hill, and E.~Zaffanella.

2016: \newblock Widening operators for powerset domains.

2017: \newblock {\em Software Tools for Technology Transfer}, 2006.

2018: \newblock To appear.

2019: 

2020: \bibitem{BagnaraRZH02}

2021: R.~Bagnara, E.~Ricci, E.~Zaffanella, and P.~M. Hill.

2022: \newblock Possibly not closed convex polyhedra and the {Parma Polyhedra

2023:   Library}.

2024: \newblock In M.~V. Hermenegildo and G.~Puebla, editors, {\em Static Analysis:

2025:   Proceedings of the 9th International Symposium}, volume 2477 of {\em Lecture

2026:   Notes in Computer Science}, pages 213--229, Madrid, Spain, 2002.

2027:   Springer-Verlag, Berlin.

2028: 

2029: \bibitem{BagnaraR-CZ05}

2030: R.~Bagnara, E.~Rodr{\'\i}guez-Carbonell, and E.~Zaffanella.

2031: \newblock Generation of basic semi-algebraic invariants using convex polyhedra.

2032: \newblock In C.~Hankin and I.~Siveroni, editors, {\em Static Analysis:

2033:   Proceedings of the 12th International Symposium}, volume 3672 of {\em Lecture

2034:   Notes in Computer Science}, pages 19--34, London, UK, 2005. Springer-Verlag,

2035:   Berlin.

2036: 

2037: \bibitem{BalasundaramK89}

2038: V.~Balasundaram and K.~Kennedy.

2039: \newblock A technique for summarizing data access and its use in parallelism

2040:   enhancing transformations.

2041: \newblock In B.~Knobe, editor, {\em Proceedings of the ACM SIGPLAN'89

2042:   Conference on Programming Language Design and Implementation (PLDI)}, volume

2043:   24(7) of {\em ACM SIGPLAN Notices}, pages 41--53, Portland, Oregon, USA,

2044:   1989. ACM Press.

2045: 

2046: \bibitem{Bellman57}

2047: R.~Bellman.

2048: \newblock {\em Dynamic Programming}.

2049: \newblock Princeton University Press, 1957.

2050: 

2051: \bibitem{BerardF99}

2052: B.~B\'erard and L.~Fribourg:.

2053: \newblock Reachability analysis of (timed) {Petri} nets using real arithmetic.

2054: \newblock In J.~C.~M. Baeten and S.~Mauw, editors, {\em CONCUR'99: Concurrency

2055:   Theory, Proceedings of the 10th International Conference}, volume 1664 of

2056:   {\em Lecture Notes in Computer Science}, pages 178--193, Eindhoven, The

2057:   Netherlands, 1999. Springer-Verlag, Berlin.

2058: 

2059: \bibitem{BlanchetCCFMMMR03}

2060: B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,

2061:   D.~Monniaux, and X.~Rival.

2062: \newblock A static analyzer for large safety-critical software.

2063: \newblock In {\em Proceedings of the ACM SIGPLAN 2003 Conference on Programming

2064:   Language Design and Implementation (PLDI'03)}, pages 196--207, San Diego,

2065:   California, USA, 2003. ACM Press.

2066: 

2067: \bibitem{BozzanoBCJRSS05}

2068: M.~Bozzano, R.~Bruttomesso, A.~Cimatti, T.~A. Junttila, P.~{van Rossum},

2069:   S.~Schulz, and R.~Sebastiani.

2070: \newblock The {MathSAT 3} system.

2071: \newblock In R.~Nieuwenhuis, editor, {\em Automated Deduction: Proceedings of

2072:   the 20th International Conference}, volume 3632 of {\em Lecture Notes in

2073:   Computer Science}, pages 315--321, Tallinn, Estonia, 2005. Springer-Verlag,

2074:   Berlin.

2075: 

2076: \bibitem{BremnerFM98}

2077: D.~Bremner, K.~Fukuda, and A.~Marzetta.

2078: \newblock Primal-dual methods for vertex and facet enumeration.

2079: \newblock {\em Discrete and Computational Geometry}, 20(3):333--357, 1998.

2080: 

2081: \bibitem{BultanGP99}

2082: T.~Bultan, R.~Gerber, and W.~Pugh.

2083: \newblock Model-checking concurrent systems with unbounded integer variables:

2084:   Symbolic representations, approximations, and experimental results.

2085: \newblock {\em ACM Transactions on Programming Languages and Systems},

2086:   21(4):747--789, 1999.

2087: 

2088: \bibitem{Chernikova64}

2089: N.~V. Chernikova.

2090: \newblock Algorithm for finding a general formula for the non-negative

2091:   solutions of system of linear equations.

2092: \newblock {\em U.S.S.R. Computational Mathematics and Mathematical Physics},

2093:   4(4):151--158, 1964.

2094: 

2095: \bibitem{Chernikova65}

2096: N.~V. Chernikova.

2097: \newblock Algorithm for finding a general formula for the non-negative

2098:   solutions of system of linear inequalities.

2099: \newblock {\em U.S.S.R. Computational Mathematics and Mathematical Physics},

2100:   5(2):228--233, 1965.

2101: 

2102: \bibitem{Chernikova68}

2103: N.~V. Chernikova.

2104: \newblock Algorithm for discovering the set of all solutions of a linear

2105:   programming problem.

2106: \newblock {\em U.S.S.R. Computational Mathematics and Mathematical Physics},

2107:   8(6):282--293, 1968.

2108: 

2109: \bibitem{Cousot81}

2110: P.~Cousot.

2111: \newblock Semantic foundations of program analysis.

2112: \newblock In S.~S. Muchnick and N.~D. Jones, editors, {\em Program Flow

2113:   Analysis: Theory and Applications}, chapter~10, pages 303--342. Prentice

2114:   Hall, Inc., Englewood Cliffs, New Jersey, 1981.

2115: 

2116: \bibitem{CousotC76}

2117: P.~Cousot and R.~Cousot.

2118: \newblock Static determination of dynamic properties of programs.

2119: \newblock In B.~Robinet, editor, {\em Proceedings of the Second International

2120:   Symposium on Programming}, pages 106--130, Paris, France, 1976. Dunod, Paris,

2121:   France.

2122: 

2123: \bibitem{CousotC77}

2124: P.~Cousot and R.~Cousot.

2125: \newblock Abstract interpretation: {A} unified lattice model for static

2126:   analysis of programs by construction or approximation of fixpoints.

2127: \newblock In {\em Proceedings of the Fourth Annual ACM Symposium on Principles

2128:   of Programming Languages}, pages 238--252, New York, 1977. ACM Press.

2129: 

2130: \bibitem{CousotC79}

2131: P.~Cousot and R.~Cousot.

2132: \newblock Systematic design of program analysis frameworks.

2133: \newblock In {\em Proceedings of the Sixth Annual ACM Symposium on Principles

2134:   of Programming Languages}, pages 269--282, New York, 1979. ACM Press.

2135: 

2136: \bibitem{CousotC92fr}

2137: P.~Cousot and R.~Cousot.

2138: \newblock Abstract interpretation frameworks.

2139: \newblock {\em Journal of Logic and Computation}, 2(4):511--547, 1992.

2140: 

2141: \bibitem{CousotC92plilp}

2142: P.~Cousot and R.~Cousot.

2143: \newblock Comparing the {Galois} connection and widening/narrowing approaches

2144:   to abstract interpretation.

2145: \newblock In M.~Bruynooghe and M.~Wirsing, editors, {\em Proceedings of the 4th

2146:   International Symposium on Programming Language Implementation and Logic

2147:   Programming}, volume 631 of {\em Lecture Notes in Computer Science}, pages

2148:   269--295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.

2149: 

2150: \bibitem{CousotCFMMMR05}

2151: P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e, D.~Monniaux, and

2152:   X.~Rival.

2153: \newblock The {ASTR\'EE} analyzer.

2154: \newblock In M.~Sagiv, editor, {\em Programming Languages and Systems,

2155:   Proceedings of the 14th European Symposium on Programming}, volume 3444 of

2156:   {\em Lecture Notes in Computer Science}, pages 21--30, Edinburgh, UK, 2005.

2157:   Springer-Verlag, Berlin.

2158: 

2159: \bibitem{CousotH78}

2160: P.~Cousot and N.~Halbwachs.

2161: \newblock Automatic discovery of linear restraints among variables of a

2162:   program.

2163: \newblock In {\em Conference Record of the Fifth Annual ACM Symposium on

2164:   Principles of Programming Languages}, pages 84--96, Tucson, Arizona, 1978.

2165:   ACM Press.

2166: 

2167: \bibitem{Davis87}

2168: E.~Davis.

2169: \newblock Constraint propagation with interval labels.

2170: \newblock {\em Artificial Intelligence}, 32(3):281--331, 1987.

2171: 

2172: \bibitem{Dill89}

2173: D.~L. Dill.

2174: \newblock Timing assumptions and verification of finite-state concurrent

2175:   systems.

2176: \newblock In J.~Sifakis, editor, {\em Proceedings of the International Workshop

2177:   on Automatic Verification Methods for Finite State Systems}, volume 407 of

2178:   {\em Lecture Notes in Computer Science}, pages 197--212, Grenoble, France,

2179:   1989. Springer-Verlag, Berlin.

2180: 

2181: \bibitem{DooseM05}

2182: D.~Doose and Z.~Mammeri.

2183: \newblock Polyhedra-based approach for incremental validation of real-time

2184:   systems.

2185: \newblock In L.~T. Yang, M.~Amamiya, Z.~Liu, M.~Guo, and F.~J. Rammig, editors,

2186:   {\em Proceedings of the International Conference on Embedded and Ubiquitous

2187:   Computing (EUC 2005)}, volume 3824 of {\em Lecture Notes in Computer

2188:   Science}, pages 184--193, Nagasaki, Japan, 2005. Springer-Verlag, Berlin.

2189: 

2190: \bibitem{DoyenHR05}

2191: L.~Doyen, T.~A. Henzinger, and J.-F. Raskin.

2192: \newblock Automatic rectangular refinement of affine hybrid systems.

2193: \newblock Technical Report 2005.47, Centre F\'ed\'er\'e en V\'erification,

2194:   Universit\'e Libre de Bruxelles, Belgium, 2005.

2195: 

2196: \bibitem{Ellenbogen04th}

2197: R.~Ellenbogen.

2198: \newblock Fully automatic verification of absence of errors via interprocedural

2199:   integer analysis.

2200: \newblock Master's thesis, School of Computer Science, Tel-Aviv University,

2201:   Tel-Aviv, Israel, December 2004.

2202: 

2203: \bibitem{Frehse04}

2204: G.~Frehse.

2205: \newblock Compositional verification of hybrid systems with discrete

2206:   interaction using simulation relations.

2207: \newblock In {\em Proceedings of the IEEE Conference on Computer Aided Control

2208:   Systems Design (CACSD 2004)}, Taipei, Taiwan, 2004.

2209: 

2210: \bibitem{Frehse05}

2211: G.~Frehse.

2212: \newblock {PHAVer}: Algorithmic verification of hybrid systems past hytech.

2213: \newblock In M.~Morari and L.~Thiele, editors, {\em Hybrid Systems: Computation

2214:   and Control: Proceedings of the 8th International Workshop (HSCC 2005)},

2215:   volume 3414 of {\em Lecture Notes in Computer Science}, pages 258--273,

2216:   Z{\"u}rich, Switzerland, 2005. Springer-Verlag, Berlin.

2217: 

2218: \bibitem{FrehseHK04}

2219: G.~Frehse, Z.~Han, and B.~Krogh.

2220: \newblock Assume-guarantee reasoning for hybrid {I/O}-automata by

2221:   over-approximation of continuous interaction.

2222: \newblock In {\em Proceedings of the 43rd IEEE Conference on Decision and

2223:   Control (CDC 2004)}, Atlantis, Paradise Island, Bahamas, 2004.

2224: 

2225: \bibitem{FrehseKR06}

2226: G.~Frehse, B.~H. Krogh, and R.~A. Rutenbar.

2227: \newblock Verifying analog oscillator circuits using forward/backward

2228:   refinement.

2229: \newblock In {\em Proceedings of the 9th Conference on Design, Automation and

2230:   Test in Europe (DATE 06)}, Munich, Germany, 2006. ACM SIGDA.

2231: \newblock {CD-ROM} publication.

2232: 

2233: \bibitem{FrehseKRM05}

2234: G.~Frehse, B.~H. Krogh, R.~A. Rutenbar, and O.~Maler.

2235: \newblock Time domain verification of oscillator circuit properties.

2236: \newblock Available at

2237:   \url{http://www-verimag.imag.fr/~maler/Papers/oscil.pdf}, 2005.

2238: \newblock Presented at the 2005 Workshop on Formal Verification of Analog

2239:   Circuits (a satellite event of ETAPS 2005).

2240: 

2241: \bibitem{FukudaP96}

2242: K.~Fukuda and A.~Prodon.

2243: \newblock Double description method revisited.

2244: \newblock In M.~Deza, R.~Euler, and Y.~Manoussakis, editors, {\em Combinatorics

2245:   and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference,

2246:   Brest, France, July 3-5, 1995, Selected Papers}, volume 1120 of {\em Lecture

2247:   Notes in Computer Science}, pages 91--111. Springer-Verlag, Berlin, 1996.

2248: 

2249: \bibitem{GopanDMDRS04}

2250: D.~Gopan, F.~DiMaio, N.~Dor, T.~Reps, and M.~Sagiv.

2251: \newblock Numeric domains with summarized dimensions.

2252: \newblock In K.~Jensen and A.~Podelski, editors, {\em Tools and Algorithms for

2253:   the Construction and Analysis of Systems, 10th International Conference,

2254:   TACAS 2004}, volume 2988 of {\em Lecture Notes in Computer Science}, pages

2255:   512--529, Barcelona, Spain, 2004. Springer-Verlag, Berlin.

2256: 

2257: \bibitem{GopanRS05}

2258: D.~Gopan, T.~Reps, and M.~Sagiv.

2259: \newblock A framework for numeric analysis of array operations.

2260: \newblock In {\em Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on

2261:   Principles of Programming Languages}, pages 338--350, Long Beach, California,

2262:   USA, 2005.

2263: 

2264: \bibitem{Granger91}

2265: P.~Granger.

2266: \newblock Static analysis of linear congruence equalities among variables of a

2267:   program.

2268: \newblock In S.~Abramsky and T.~S.~E. Maibaum, editors, {\em TAPSOFT'91:

2269:   Proceedings of the International Joint Conference on Theory and Practice of

2270:   Software Development, Volume 1: Colloquium on Trees in Algebra and

2271:   Programming (CAAP'91)}, volume 493 of {\em Lecture Notes in Computer

2272:   Science}, pages 169--192, Brighton, UK, 1991. Springer-Verlag, Berlin.

2273: 

2274: \bibitem{Granger97}

2275: P.~Granger.

2276: \newblock Static analyses of congruence properties on rational numbers

2277:   (extended abstract).

2278: \newblock In P.~{Van Hentenryck}, editor, {\em Static Analysis: Proceedings of

2279:   the 4th International Symposium}, volume 1302 of {\em Lecture Notes in

2280:   Computer Science}, pages 278--292, Paris, France, 1997. Springer-Verlag,

2281:   Berlin.

2282: 

2283: \bibitem{Halbwachs79th}

2284: N.~Halbwachs.

2285: \newblock {\em D\'etermination Automatique de Relations Lin\'eaires

2286:   V\'erifi\'ees par les Variables d'un Programme}.

2287: \newblock {Th\`ese de 3\textsuperscript{\`eme} cycle d'informatique},

2288:   Universit\'e scientifique et m\'edicale de Grenoble, Grenoble, France, March

2289:   1979.

2290: 

2291: \bibitem{Halbwachs93}

2292: N.~Halbwachs.

2293: \newblock Delay analysis in synchronous programs.

2294: \newblock In C.~Courcoubetis, editor, {\em Computer Aided Verification:

2295:   Proceedings of the 5th International Conference}, volume 697 of {\em Lecture

2296:   Notes in Computer Science}, pages 333--346, Elounda, Greece, 1993.

2297:   Springer-Verlag, Berlin.

2298: 

2299: \bibitem{HalbwachsKP95}

2300: N.~Halbwachs, A.~Kerbrat, and Y.-E. Proy.

2301: \newblock {\em {POLyhedra INtegrated Environment}}.

2302: \newblock Verimag, France, version 1.0 of {POLINE} edition, September 1995.

2303: \newblock Documentation taken from source code.

2304: 

2305: \bibitem{HalbwachsMP-V03}

2306: N.~Halbwachs, D.~Merchat, and C.~Parent-Vigouroux.

2307: \newblock Cartesian factoring of polyhedra in linear relation analysis.

2308: \newblock In R.~Cousot, editor, {\em Static Analysis: Proceedings of the 10th

2309:   International Symposium}, volume 2694 of {\em Lecture Notes in Computer

2310:   Science}, pages 355--365, San Diego, California, USA, 2003. Springer-Verlag,

2311:   Berlin.

2312: 

2313: \bibitem{HalbwachsPR94}

2314: N.~Halbwachs, Y.-E. Proy, and P.~Raymond.

2315: \newblock Verification of linear hybrid systems by means of convex

2316:   approximations.

2317: \newblock In B.~{Le Charlier}, editor, {\em Static Analysis: Proceedings of the

2318:   1st International Symposium}, volume 864 of {\em Lecture Notes in Computer

2319:   Science}, pages 223--237, Namur, Belgium, 1994. Springer-Verlag, Berlin.

2320: 

2321: \bibitem{HalbwachsPR97}

2322: N.~Halbwachs, Y.-E. Proy, and P.~Roumanoff.

2323: \newblock Verification of real-time systems using linear relation analysis.

2324: \newblock {\em Formal Methods in System Design}, 11(2):157--185, 1997.

2325: 

2326: \bibitem{HenzingerH95}

2327: T.~A. Henzinger and P.-H. Ho.

2328: \newblock A note on abstract interpretation strategies for hybrid automata.

2329: \newblock In P.~J. Antsaklis, W.~Kohn, A.~Nerode, and S.~Sastry, editors, {\em

2330:   Hybrid Systems II}, volume 999 of {\em Lecture Notes in Computer Science},

2331:   pages 252--264. Springer-Verlag, Berlin, 1995.

2332: 

2333: \bibitem{HenzingerHW97b}

2334: T.~A. Henzinger, P.-H. Ho, and H.~Wong-Toi.

2335: \newblock {\sc HyTech}: A model checker for hybrid systems.

2336: \newblock {\em Software Tools for Technology Transfer}, 1(1+2):110--122, 1997.

2337: 

2338: \bibitem{HenzingerPW01}

2339: T.~A. Henzinger, J.~Preussig, and H.~Wong-Toi.

2340: \newblock Some lessons from the {\sc hytech} experience.

2341: \newblock In {\em Proceedings of the 40th Annual Conference on Decision and

2342:   Control}, pages 2887--2892. IEEE Computer Society Press, 2001.

2343: 

2344: \bibitem{HymansU04}

2345: C.~Hymans and E.~Upton.

2346: \newblock Static analysis of gated data dependence graphs.

2347: \newblock In R.~Giacobazzi, editor, {\em Static Analysis: Proceedings of the

2348:   11th International Symposium}, volume 3148 of {\em Lecture Notes in Computer

2349:   Science}, pages 197--211, Verona, Italy, 2004. Springer-Verlag, Berlin.

2350: 

2351: \bibitem{NEW-POLKA-1-1-3c}

2352: B.~Jeannet.

2353: \newblock {\em Convex Polyhedra Library}, release 1.1.3c edition, March 2002.

2354: \newblock Documentation of the ``New Polka'' library available at

2355:   \url{http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html}.

2356: 

2357: \bibitem{KruegelKMRV05}

2358: C.~Kruegel, E.~Kirda, D.~Mutz, W.~Robertson, and G.~Vigna.

2359: \newblock Automating mimicry attacks using static binary analysis.

2360: \newblock In {\em Proceedings of Security~'05, the 14th USENIX Security

2361:   Symposium}, pages 161--176, Baltimore, MD, USA, 2005.

2362: 

2363: \bibitem{LarsenLPY97}

2364: K.~Larsen, F.~Larsson, P.~Pettersson, and W.~Yi.

2365: \newblock Efficient verification of real-time systems: Compact data structure

2366:   and state-space reduction.

2367: \newblock In {\em Proceedings of the 18th IEEE Real-Time Systems Symposium

2368:   (RTSS'97)}, pages 14--24, San Francisco, CA, 1997. IEEE Computer Society

2369:   Press.

2370: 

2371: \bibitem{LeVerge92}

2372: H.~{Le Verge}.

2373: \newblock A note on {Chernikova's} algorithm.

2374: \newblock \emph{Publication interne} 635, IRISA, Campus de Beaulieu, Rennes,

2375:   France, 1992.

2376: 

2377: \bibitem{Loechner99}

2378: V.~Loechner.

2379: \newblock {\it PolyLib\/}: A library for manipulating parameterized polyhedra.

2380: \newblock Available at \url{http://icps.u-strasbg.fr/~loechner/polylib/}, March

2381:   1999.

2382: \newblock Declares itself to be a continuation of \cite{Wilde93th}.

2383: 

2384: \bibitem{MesnardB05TPLP}

2385: F.~Mesnard and R.~Bagnara.

2386: \newblock {cTI}: A constraint-based termination inference tool for

2387:   {ISO-Prolog}.

2388: \newblock {\em Theory and Practice of Logic Programming}, 5(1{\&}2):243--257,

2389:   2005.

2390: 

2391: \bibitem{Mine01b}

2392: A.~Min\'e.

2393: \newblock The octagon abstract domain.

2394: \newblock In {\em Proceedings of the Eighth Working Conference on Reverse

2395:   Engineering (WCRE'01)}, pages 310--319, Stuttgart, Germany, 2001. IEEE

2396:   Computer Society Press.

2397: 

2398: \bibitem{Mine05th}

2399: A.~Min\'e.

2400: \newblock {\em Weakly Relational Numerical Abstract Domains}.

2401: \newblock PhD thesis, \'Ecole Polytechnique, Paris, France, March 2005.

2402: 

2403: \bibitem{MotzkinRTT53}

2404: T.~S. Motzkin, H.~Raiffa, G.~L. Thompson, and R.~M. Thrall.

2405: \newblock The double description method.

2406: \newblock In H.~W. Kuhn and A.~W. Tucker, editors, {\em Contributions to the

2407:   Theory of Games -- Volume II}, number~28 in Annals of Mathematics Studies,

2408:   pages 51--73. Princeton University Press, Princeton, New Jersey, 1953.

2409: 

2410: \bibitem{NakanishiF01}

2411: T.~Nakanishi and A.~Fukuda.

2412: \newblock Modulo interval arithmetic and its application to program analysis.

2413: \newblock {\em Transactions of Information Processing Society of Japan},

2414:   42(4):829--837, 2001.

2415: 

2416: \bibitem{NakanishiJPF99}

2417: T.~Nakanishi, K.~Joe, C.~D. Polychronopoulos, and A.~Fukuda.

2418: \newblock The modulo interval: A simple and practical representation for

2419:   program analysis.

2420: \newblock In {\em Proceedings of the 1999 International Conference on Parallel

2421:   Architectures and Compilation Techniques}, pages 91--96, Newport Beach,

2422:   California, USA, 1999. IEEE Computer Society.

2423: 

2424: \bibitem{NemhauserW88}

2425: G.~L. Nemhauser and L.~A. Wolsey.

2426: \newblock {\em Integer and Combinatorial Optimization}.

2427: \newblock Wiley Interscience Series in Discrete Mathematics and Optimization.

2428:   John Wiley \& Sons, 1988.

2429: 

2430: \bibitem{QuintonRR96}

2431: P.~Quinton, S.~Rajopadhye, and T.~Risset.

2432: \newblock On manipulating {Z}-polyhedra.

2433: \newblock Technical Report 1016, IRISA, Campus Universitaire de Bealieu,

2434:   Rennes, France, July 1996.

2435: 

2436: \bibitem{QuintonRR97}

2437: P.~Quinton, S.~Rajopadhye, and T.~Risset.

2438: \newblock On manipulating {Z}-polyhedra using a canonic representation.

2439: \newblock {\em Parallel Processing Letters}, 7(2):181--194, 1997.

2440: 

2441: \bibitem{SankaranarayananCSM06}

2442: S.~Sankaranarayanan, M.~Col{\'o}n, H.~B. Sipma, and Z.~Manna.

2443: \newblock Efficient strongly relational polyhedral analysis.

2444: \newblock In E.~A. Emerson and K.~S. Namjoshi, editors, {\em Verification,

2445:   Model Checking and Abstract Interpretation: Proceedings of the 7th

2446:   International Conference (VMCAI 2006)}, volume 3855 of {\em Lecture Notes in

2447:   Computer Science}, pages 111--125, Charleston, SC, USA, 2006.

2448:   Springer-Verlag, Berlin.

2449: 

2450: \bibitem{SankaranarayananSM04}

2451: S.~Sankaranarayanan, H.~B. Sipma, and Z.~Manna.

2452: \newblock Constraint-based linear-relations analysis.

2453: \newblock In R.~Giacobazzi, editor, {\em Static Analysis: Proceedings of the

2454:   11th International Symposium}, volume 3148 of {\em Lecture Notes in Computer

2455:   Science}, pages 53--68, Verona, Italy, 2004. Springer-Verlag, Berlin.

2456: 

2457: \bibitem{SankaranarayananSM05}

2458: S.~Sankaranarayanan, H.~B. Sipma, and Z.~Manna.

2459: \newblock Scalable analysis of linear systems using mathematical programming.

2460: \newblock In R.~Cousot, editor, {\em Verification, Model Checking and Abstract

2461:   Interpretation: Proceedings of the 6th International Conference (VMCAI

2462:   2005)}, volume 3385 of {\em Lecture Notes in Computer Science}, pages 25--41,

2463:   Paris, France, 2005. Springer-Verlag, Berlin.

2464: 

2465: \bibitem{SankaranarayananSM06}

2466: S.~Sankaranarayanan, H.~B. Sipma, and Z.~Manna.

2467: \newblock Fixed point iteration for computing the time elapse operator.

2468: \newblock In J.~Hespanha and A.~Tiwari, editors, {\em Hybrid Systems:

2469:   Computation and Control: Proceedings of the 9th International Workshop (HSCC

2470:   2006)}, volume 3927 of {\em Lecture Notes in Computer Science}, pages

2471:   537--551, Santa Barbara, CA, USA, 2006. Springer-Verlag, Berlin.

2472: 

2473: \bibitem{ShahamKS00}

2474: R.~Shaham, E.~K. Kolodner, and S.~Sagiv.

2475: \newblock Automatic removal of array memory leaks in {J}ava.

2476: \newblock In D.~A. Watt, editor, {\em Proceedings of the 9th International

2477:   Conference on Compiler Construction (CC 2000)}, volume 1781 of {\em Lecture

2478:   Notes in Computer Science}, pages 50--66, Berlin, Germany, 2000.

2479:   Springer-Verlag, Berlin.

2480: 

2481: \bibitem{SongCR05}

2482: H.~Song, K.~Compton, and W.~Rounds.

2483: \newblock {SPHIN:} a model checker for reconfigurable hybrid systems based on

2484:   {SPIN}.

2485: \newblock In R.~Lazic and R.~Nagarajan, editors, {\em Proceedings of the 5rd

2486:   Workshop on Automated Verification of Critical Systems}, University of

2487:   Warwick, UK, 2005.

2488: 

2489: \bibitem{StoerW70}

2490: J.~Stoer and C.~Witzgall.

2491: \newblock {\em Convexity and Optimization in Finite Dimensions I}.

2492: \newblock Springer-Verlag, Berlin, 1970.

2493: 

2494: \bibitem{vanHeeOSV06}

2495: K.~{van Hee}, O.~Oanea, N.~Sidorova, and M.~Voorhoeve.

2496: \newblock Verifying generalized soundness for workflow nets.

2497: \newblock In I.~Virbitskaite and A.~Voronkov, editors, {\em Perspectives of

2498:   System Informatics: Proceedings of the Sixth International Andrei Ershov

2499:   Memorial Conference}, Lecture Notes in Computer Science, Akademgorodok,

2500:   Novosibirsk, Russia, 2006. Springer-Verlag, Berlin.

2501: \newblock To appear.

2502: 

2503: \bibitem{VenetB04}

2504: A.~Venet and G.~Brat.

2505: \newblock Precise and efficient static array bound checking for large embedded

2506:   {C} programs.

2507: \newblock In {\em Proceedings of the ACM SIGPLAN 2004 Conference on Programming

2508:   Language Design and Implementation (PLDI'04)}, pages 231--242, Washington,

2509:   DC, USA, 2004. ACM Press.

2510: 

2511: \bibitem{Wilde93th}

2512: D.~K. Wilde.

2513: \newblock A library for doing polyhedral operations.

2514: \newblock {Master's thesis}, Oregon State University, Corvallis, Oregon,

2515:   December 1993.

2516: \newblock Also published as IRISA \emph{Publication interne} 785, Rennes,

2517:   France, 1993.

2518: 

2519: \end{thebibliography}

2520: 

2521: \begin{comment}

2522: \appendix

2523: 

2524: \section{Notes for the Editor and the Reviewers}

2525: 

2526: The source and binary distributions of all versions of the

2527: Parma Polyhedra Library are available at

2528: {\small

2529: \begin{verbatim}

2530: http://www.cs.unipr.it/ppl/Download/ftp/

2531: \end{verbatim}

2532: }

2533: The latest released version is at

2534: {\small

2535: \begin{verbatim}

2536: http://www.cs.unipr.it/ppl/Download/ftp/releases/LATEST/

2537: \end{verbatim}

2538: }

2539: 

2540: Concerning example applications, a number of them are available from the

2541: web sites of the respective authors.  For instance:

2542: \begin{itemize}

2543: \item

2544: PHAVer (Polyhedral Hybrid Automaton Verifyer) is available at

2545: \url{http://www.cs.ru.nl/~goranf/};

2546: \item

2547: StInG (Stanford Invariant Generator) is available at

2548: \url{http://theory.stanford.edu/~srirams/Software/sting.html};

2549: \item

2550: LPInv (Linear Programming Invariant Generator) is available at

2551: \url{http://theory.stanford.edu/~srirams/Software/lpinv.html}.

2552: \end{itemize}

2553: 

2554: In order to work with the CVS versions of the PPL, recent versions of GNU's

2555: Autoconf, Automake and Libtool are required: issuing the

2556: \verb+autoreconf+ command in the root directory (which is named

2557: \verb+ppl+) is enough to obtain a fully functional source tree.

2558: Alternatively, the reviewers could tell the editor to ask us to build a

2559: ``snapshot release'', which we would prepare and either forward to the

2560: editor or upload to

2561: \url{ftp://ftp.cs.unipr.it/pub/ppl/snapshots}.

2562: \end{comment}

2563: 

2564: \end{document}

2565: