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{elsart}
17: \documentclass[final]{elsart}
18:
19: %\journal{Theoretical Computer Science}
20: \date{}
21: %\received{July 4, 2007}
22: %\revised{August 30, 2007}
23: %\revised{April 9, 2008}
24:
25: % Trick to circumvent a conflict between elsart and amsmath.
26: % Suggested by Simon Pepping <S.PEPPING@elsevier.nl>
27: % on Monday, 13 May 1996.
28: \mathchardef\Omega="700A
29:
30: \usepackage{verbatim}
31: \usepackage{graphicx}
32: \usepackage[noabbrv]{unitsdef}
33: \usepackage{url}
34: \usepackage{amsmath}
35: \usepackage{amssymb}
36: \usepackage{latexsym}
37: \usepackage{stmaryrd}
38: \usepackage{rotating}
39: \usepackage{pstricks,pst-node,pst-plot,pst-circ}
40: \usepackage{subfigure}
41: \usepackage{graphicx}
42:
43: \newboolean{TR}
44: \setboolean{TR}{true}
45: %\setboolean{TR}{false}
46:
47: %% Colors.
48: \newcmykcolor{dblue}{1 1 0 .3}
49:
50: %\newcommand*{\coanote}[1]{\footnote{\textbf{For co-authors:} {#1}}}
51: \newcommand*{\coanote}[1]{}
52: \newcommand*{\TRfootnote}[1]{\ifthenelse{\boolean{TR}}{\footnote{#1}}{}}
53:
54: \newtheorem{theorem}{Theorem}[section]
55: \newtheorem{lemma}[theorem]{Lemma}
56:
57: \theoremstyle{definition}
58: \newtheorem{definition}[theorem]{Definition}
59: \newtheorem{example}[theorem]{Example}
60:
61: %% Summaries for theorem-like environments
62: \newcommand{\summary}[1]{\textrm{\textbf{\textup{#1}}}}
63:
64: \theoremstyle{remark}
65: \newtheorem{remark}[theorem]{Remark}
66:
67: \numberwithin{equation}{section}
68:
69: %% Proof trees.
70: \input prooftree
71:
72: %% Base sets.
73: \newcommand*{\ttv}{\mathrm{tt}}
74: \newcommand*{\ffv}{\mathrm{ff}}
75:
76: %% BNF rules.
77: \newcommand*{\vbar}{\mathrel{\mid}}
78:
79: %% Keywords.
80: \newcommand*{\kw}[1]{\mathop{\textbf{#1}}}
81:
82: %% Abstract syntax of the analyzed language.
83: \newcommand*{\Int}{\mathrm{Int}}
84: \newcommand*{\Bool}{\mathrm{Bool}}
85: \newcommand*{\Var}{\mathrm{Var}}
86: \newcommand*{\Aexp}{\mathrm{Aexp}}
87: \newcommand*{\Bexp}{\mathrm{Bexp}}
88: \newcommand*{\Stmt}{\mathrm{Stmt}}
89: \newcommand*{\Store}{\mathord{\mathrm{Store}}}
90:
91: \newcommand*{\eval}[2]{\mathrel{\buildrel \mathrm{#2} \over #1}}
92: \newcommand*{\ceval}[1]{\eval{\rightarrow}{#1}}
93: \newcommand*{\aceval}{\ceval{a}}
94: \newcommand*{\bceval}{\ceval{b}}
95: \newcommand*{\sceval}{\ceval{s}}
96: \newcommand*{\diverges}{\ceval{\infty}\mathord{}}
97: \newcommand*{\aeval}[1]{\eval{\rightsquigarrow}{#1}}
98: \newcommand*{\aaeval}{\aeval{a}}
99: \newcommand*{\baeval}{\aeval{b}}
100: \newcommand*{\saeval}{\aeval{s}}
101:
102: %% Abstract operators.
103: \newcommand*{\absplus}{\mathbin{\varoplus}}
104: \newcommand*{\absminus}{\mathbin{\varominus}}
105: \newcommand*{\absprod}{\mathbin{\varoast}}
106: \newcommand*{\absneg}{\mathop{\varobslash}\nolimits}
107: \newcommand*{\absor}{\mathbin{\varovee}}
108: \newcommand*{\absand}{\mathbin{\varowedge}}
109: \newcommand*{\abseq}{\mathrel{\varocircle}}
110: \newcommand*{\abslt}{\mathrel{\varolessthan}}
111:
112: \newcommand*{\nohyp}{\phantom{\langle a_0, \sigma \rangle \aceval m_0}}
113: \newcommand*{\omissis}{\left[\,\mathord{\cdots}\,\right]}
114:
115: %% \newcommand*{\Con}{\mathrm{Con}}
116: \newcommand*{\con}{\mathrm{con}}
117: \newcommand*{\gen}{\mathrm{gen}}
118: %% \newcommand*{\fps}{\mathrm{fps}}
119: %% \newcommand*{\emptysequence}{\boxempty}
120:
121: %% Convex polyhedral hull.
122: \newcommand{\polyhull}{\mathbin{\uplus}}
123: % Generic widening
124: \newcommand*{\widen}{\mathbin{\nabla}}
125:
126: %% Things that hold by definition.
127: \newcommand{\defrel}[1]{\mathrel{\buildrel \mathrm{def} \over {#1}}}
128: \newcommand{\defeq}{\defrel{=}}
129: \newcommand{\defiff}{\defrel{\Longleftrightarrow}}
130: %\newcommand{\defeq}{=}
131: %\newcommand{\defiff}{\Longleftrightarrow}
132:
133: %% Special letters denoting sets and algebras.
134: \providecommand*{\Nset}{\mathbb{N}} % Naturals
135: \providecommand*{\Qset}{\mathbb{Q}} % Rationals
136: \providecommand*{\Zset}{\mathbb{Z}} % Integers
137: \providecommand*{\Rset}{\mathbb{R}} % Reals
138: \providecommand*{\nonnegRset}{\mathbb{R}_{\scriptscriptstyle{+}}}
139: % Non-negative reals
140:
141: \newcommand{\sset}[2]{{\renewcommand{\arraystretch}{1.2}
142: \left\{\,#1 \,\left|\,
143: \begin{array}{@{}l@{}}#2\end{array}
144: \right. \,\right\}}}
145:
146: %% Subset and supset relations
147: \newcommand*{\sseq}{\subseteq}
148: %%\newcommand*{\sseqf}{\mathrel{\subseteq_\mathrm{f}}}
149: \newcommand*{\sslt}{\subset}
150: \newcommand*{\Sseq}{\supseteq}
151: \newcommand*{\Ssgt}{\supset}
152: \newcommand{\Nsseq}{\nsubseteq}
153:
154: %% Set operations
155: \newcommand*{\union}{\cup}
156: \newcommand*{\bigunion}{\bigcup}
157: \newcommand*{\biginters}{\bigcap}
158: \newcommand*{\inters}{\cap}
159: \newcommand*{\setdiff}{\setminus}
160:
161: % square subset and supset relations
162: \newcommand*{\sqsseq}{\sqsubseteq}
163:
164: % Least fixpoint.
165: \newcommand*{\lfp}{\mathop{\mathrm{lfp}}\nolimits}
166:
167: %% Matrix and vector functions.
168: \newcommand*{\mat}{\mathop{\mathrm{matrix}}\nolimits}
169: \newcommand*{\transpose}{{\scriptscriptstyle\mathrm{T}}}
170: %\newcommand*{\vect}[1]{\vec{#1}}
171: \newcommand*{\vect}[1]{\mathbf{#1}}
172:
173: %% Logical quantifiers stuff
174: \newcommand{\st}{\mathrel{.}}
175: \newcommand{\itc}{\mathrel{:}}
176:
177: %% Logic notation
178: \newcommand*{\entails}{\mathrel{\vdash}}
179: \newcommand*{\bigland}{\mathop{\bigwedge}}
180: \newcommand*{\biglor}{\mathop{\bigvee}}
181:
182: %% Lambda notation
183: \newcommand{\lambdadot}{\mathbin{.}}
184:
185: %% Relational operator.
186: \newcommand{\relop}{\mathrel{\bowtie}}
187:
188: %% Calligraphic alphabet
189: \newcommand*{\cA}{\ensuremath{\mathcal{A}}}
190: \newcommand*{\cB}{\ensuremath{\mathcal{B}}}
191: \newcommand*{\cC}{\ensuremath{\mathcal{C}}}
192: \newcommand*{\cD}{\ensuremath{\mathcal{D}}}
193: \newcommand*{\cE}{\ensuremath{\mathcal{E}}}
194: \newcommand*{\cF}{\ensuremath{\mathcal{F}}}
195: \newcommand*{\cG}{\ensuremath{\mathcal{G}}}
196: \newcommand*{\cH}{\ensuremath{\mathcal{H}}}
197: \newcommand*{\cI}{\ensuremath{\mathcal{I}}}
198: \newcommand*{\cJ}{\ensuremath{\mathcal{J}}}
199: \newcommand*{\cK}{\ensuremath{\mathcal{K}}}
200: \newcommand*{\cL}{\ensuremath{\mathcal{L}}}
201: \newcommand*{\cM}{\ensuremath{\mathcal{M}}}
202: \newcommand*{\cN}{\ensuremath{\mathcal{N}}}
203: \newcommand*{\cO}{\ensuremath{\mathcal{O}}}
204: \newcommand*{\cP}{\ensuremath{\mathcal{P}}}
205: \newcommand*{\cQ}{\ensuremath{\mathcal{Q}}}
206: \newcommand*{\cR}{\ensuremath{\mathcal{R}}}
207: \newcommand*{\cS}{\ensuremath{\mathcal{S}}}
208: \newcommand*{\cT}{\ensuremath{\mathcal{T}}}
209: \newcommand*{\cU}{\ensuremath{\mathcal{U}}}
210: \newcommand*{\cV}{\ensuremath{\mathcal{V}}}
211: \newcommand*{\cW}{\ensuremath{\mathcal{W}}}
212: \newcommand*{\cX}{\ensuremath{\mathcal{X}}}
213: \newcommand*{\cY}{\ensuremath{\mathcal{Y}}}
214: \newcommand*{\cZ}{\ensuremath{\mathcal{Z}}}
215:
216: %% Declarators for functions and relations
217: \newcommand*{\reld}[3]{\mathord{#1}\subseteq#2\times#3}
218: \newcommand*{\fund}[3]{\mathord{#1}\colon#2\rightarrow#3}
219: \newcommand*{\pard}[3]{\mathord{#1}\colon#2\rightarrowtail#3}
220:
221: %% Composition of functions
222: \newcommand*{\compose}{\mathbin{\circ}}
223:
224: %% Domains
225: \providecommand*{\CPset}{\mathbb{CP}} % Closed polyhedra
226: \providecommand*{\Pset}{\mathbb{P}} % (NNC) polyhedra
227: \providecommand*{\Gset}{\mathbb{G}} % Rational Lattice
228:
229: %% Extras needed for hybrid systems
230: \newcommand*{\Loc}{\mathrm{Loc}}
231: \newcommand*{\Lab}{\mathrm{Lab}}
232: \newcommand*{\Init}{\mathrm{Init}}
233: \newcommand*{\Trans}{\mathrm{Trans}}
234: \newcommand*{\Inv}{\mathrm{Inv}}
235: \newcommand*{\Act}{\mathrm{Act}}
236: \newcommand*{\Reach}{\mathrm{Reach}}
237: \newcommand*{\Lset}{\mathbb{L}}
238: \newcommand*{\timeelapse}{\nearrow}
239:
240: %% Used in examples of hybrid systems.
241: \newcommand*{\plusplus}{\mathord{\scriptstyle ++}}
242: \newcommand*{\minusminus}{\mathord{\scriptstyle --}}
243:
244: % The set of rays of a polyhedron.
245: \newcommand*{\rays}{\mathop{\mathrm{rays}}\nolimits}
246: % The set of lines of a polyhedron.
247: \newcommand*{\lines}{\mathop{\mathrm{lines}}\nolimits}
248:
249: %% The set of equality and inequality constraints in a constraint system.
250: \newcommand*{\eq}{\mathop{\mathrm{eq}}\nolimits}
251: \newcommand*{\ineq}{\mathop{\mathrm{ineq}}\nolimits}
252:
253: \newcommand*{\timedstep}[2]{\mathrel{\rightarrow^{#1}_{#2}}}
254:
255: %% Domain and co-domain of a function
256: \newcommand*{\dom}{\mathop{\mathrm{dom}}\nolimits}
257: \newcommand*{\cod}{\mathop{\mathrm{cod}}\nolimits}
258:
259: \hyphenation{%
260: %% From the AMS packages
261: acad-e-my acad-e-mies af-ter-thought anom-aly anom-alies
262: an-ti-deriv-a-tive an-tin-o-my an-tin-o-mies apoth-e-o-ses
263: apoth-e-o-sis ap-pen-dix ar-che-typ-al as-sign-a-ble as-sist-ant-ship
264: as-ymp-tot-ic asyn-chro-nous at-trib-uted at-trib-ut-able bank-rupt
265: bank-rupt-cy bi-dif-fer-en-tial blue-print busier busiest
266: cat-a-stroph-ic cat-a-stroph-i-cally con-gress cross-hatched data-base
267: de-fin-i-tive de-riv-a-tive dis-trib-ute dri-ver dri-vers eco-nom-ics
268: econ-o-mist elit-ist equi-vari-ant ex-quis-ite ex-tra-or-di-nary
269: flow-chart for-mi-da-ble forth-right friv-o-lous ge-o-des-ic
270: ge-o-det-ic geo-met-ric griev-ance griev-ous griev-ous-ly
271: hexa-dec-i-mal ho-lo-no-my ho-mo-thetic ideals idio-syn-crasy
272: in-fin-ite-ly in-fin-i-tes-i-mal ir-rev-o-ca-ble key-stroke
273: lam-en-ta-ble light-weight mal-a-prop-ism man-u-script mar-gin-al
274: meta-bol-ic me-tab-o-lism meta-lan-guage me-trop-o-lis
275: met-ro-pol-i-tan mi-nut-est mol-e-cule mono-chrome mono-pole
276: mo-nop-oly mono-spline mo-not-o-nous mul-ti-fac-eted mul-ti-plic-able
277: non-euclid-ean non-iso-mor-phic non-smooth par-a-digm par-a-bol-ic
278: pa-rab-o-loid pa-ram-e-trize para-mount pen-ta-gon phe-nom-e-non
279: post-script pre-am-ble pro-ce-dur-al pro-hib-i-tive pro-hib-i-tive-ly
280: pseu-do-dif-fer-en-tial pseu-do-fi-nite pseu-do-nym qua-drat-ic
281: quad-ra-ture qua-si-smooth qua-si-sta-tion-ary qua-si-tri-an-gu-lar
282: quin-tes-sence quin-tes-sen-tial re-arrange-ment rec-tan-gle
283: ret-ri-bu-tion retro-fit retro-fit-ted right-eous right-eous-ness
284: ro-bot ro-bot-ics sched-ul-ing se-mes-ter semi-def-i-nite
285: semi-ho-mo-thet-ic set-up se-vere-ly side-step sov-er-eign spe-cious
286: spher-oid spher-oid-al star-tling star-tling-ly sta-tis-tics
287: sto-chas-tic straight-est strange-ness strat-a-gem strong-hold
288: sum-ma-ble symp-to-matic syn-chro-nous topo-graph-i-cal tra-vers-a-ble
289: tra-ver-sal tra-ver-sals treach-ery turn-around un-at-tached
290: un-err-ing-ly white-space wide-spread wing-spread wretch-ed
291: wretch-ed-ly Eng-lish Euler-ian Feb-ru-ary Gauss-ian
292: Hamil-ton-ian Her-mit-ian Jan-u-ary Japan-ese Kor-te-weg
293: Le-gendre Mar-kov-ian Noe-ther-ian No-vem-ber Rie-mann-ian Sep-tem-ber
294: %% Added myself
295: Ba-gna-ra Zaf-fa-nel-la Par-ma
296: }
297:
298: \begin{document}
299:
300: \begin{frontmatter}
301:
302: \title%
303: %[Polyhedral Computations and HW/SW Analysis and Verification]%
304: {Applications of Polyhedral Computations \\
305: to the Analysis and Verification \\
306: of Hardware and Software Systems\thanksref{th}}
307:
308: \thanks[th]{This work has been partly supported by PRIN project
309: ``AIDA: Abstract Interpretation Design and Applications.''}
310:
311: \author[Parma]{Roberto Bagnara},
312: \ead{bagnara@cs.unipr.it}
313: \author[Leeds]{Patricia M. Hill},
314: \ead{hill@comp.leeds.ac.uk}
315: \author[Parma]{Enea Zaffanella}
316: \ead{zaffanella@cs.unipr.it}
317:
318: \address[Parma]{Department of Mathematics, University of Parma, Italy}
319: \address[Leeds]{School of Computing, University of Leeds, UK}
320:
321: \begin{abstract}
322: Convex polyhedra are the basis for several abstractions used in static
323: analysis and computer-aided verification of complex and sometimes
324: mission critical systems. For such applications, the identification of
325: an appropriate complexity-precision trade-off is a particularly acute
326: problem, so that the availability of a wide spectrum of alternative
327: solutions is mandatory. We survey the range of applications of
328: polyhedral computations in this area; give an overview of the
329: different classes of polyhedra that may be adopted;
330: outline the main polyhedral operations required by
331: automatic analyzers and verifiers; and look at some possible
332: combinations of polyhedra with other numerical abstractions that have
333: the potential to improve the precision of the analysis.
334: Areas where
335: further theoretical investigations can result in important
336: contributions are highlighted.
337: \end{abstract}
338:
339: \begin{keyword}
340: Static analysis, computer-aided verification, abstract interpretation.
341: \end{keyword}
342:
343: \end{frontmatter}
344:
345: \section{Introduction}
346: \label{sec:introduction}
347:
348: The application of polyhedral computations to the analysis and
349: verification of computer programs has its origin in a groundbreaking
350: paper by Cousot and Halbwachs \cite{CousotH78}.
351: There, the authors applied the theory of abstract interpretation
352: \ifthenelse{\boolean{TR}}{%%
353: \cite{CousotC77,CousotC92fr}
354: }{%%
355: \cite{CousotC79,CousotC92fr}
356: }%%\ifthenelse{\boolean{TR}}
357: to the static determination of linear equality and inequality
358: relations among program variables. In essence, the idea consists
359: in interpreting a program (as will be explained in more detail in
360: Sections~\ref{sec:abstract-interpretation}
361: and~\ref{sec:analysis-of-computer-programs})
362: on a domain of convex polyhedra instead of the concrete domain
363: of (sets of vectors of) machine numbers. Each program operation is
364: correctly approximated by a corresponding operation on polyhedra
365: and measures are taken to ensure that the approximate computation
366: always terminates. At the end of this process, the obtained
367: polyhedra encode provably correct \emph{linear invariants} of the
368: analyzed program (i.e., linear equalities and inequalities that are
369: guaranteed to hold for each program execution and for each program input).
370:
371: As we show in this paper, relational information
372: concerning the data objects manipulated by programs or other devices
373: is crucial for a broad range of applications in the field
374: of automatic or semi-automatic program manipulation: it can be used to prove
375: the absence of certain kinds of errors; it can verify that certain processes
376: always terminate or stabilize; it can pinpoint the position of
377: errors in the system;
378: and it can enable the application of optimizations.
379: Despite this, due to the lack of efficient, robust and publicly available
380: implementations of convex polyhedra and of the required operations,
381: the line of work begun by Cousot and Halbwachs did not see much
382: development until the beginning of the 1990s. Since then, this
383: approach has been increasingly adopted and today convex polyhedra
384: are the basis for several abstractions used in static analysis and
385: computer-aided verification of complex and sometimes mission critical
386: systems. For such applications, the identification of an appropriate
387: complexity-precision trade-off is a particularly acute problem:
388: on the one hand, relational information provided by general polyhedra
389: is extremely valuable; on the other hand, its high computational cost
390: makes it a fairly scarce resource that must be managed with care.
391: This implies, among other things, that general polyhedra must be
392: combined with simpler polyhedra in order to achieve scalability.
393: As the complexity-precision trade-off varies considerably between
394: different applications, the availability of a wide spectrum of alternative
395: solutions is mandatory.
396:
397: In this paper, we survey the range of applications of polyhedral
398: computations in the area of the analysis and verification of hardware
399: and software systems:
400: we describe in detail one important ---and historically, first--- application
401: of polyhedral computations in the field of formal methods,
402: the linear invariant analysis for imperative programs;
403: we provide an account of linear hybrid systems that is based directly on
404: polyhedra;
405: and we explain with an example how polyhedral approximations
406: can be applied to analog systems.
407: The paper also provides
408: an overview of the main polyhedral operations required by these applications,
409: brief descriptions of some of the different classes of
410: polyhedra that may be adopted, depending on the particular context,
411: and a look at some possible combinations of
412: polyhedra with other numerical abstractions that have the potential to
413: improve the precision of the analysis.
414: Areas where further theoretical investigations can result
415: in important contributions are highlighted.
416: \ifthenelse{\boolean{TR}}{}{%%
417: Some bibliographic references and a few examples have been omitted
418: from this paper for space reasons; the interested reader can find them
419: in the technical report version~\cite{BagnaraHZ07TRa}.
420: }%%\ifthenelse{\boolean{TR}}{}{%%
421:
422: The plan of the paper is as follows.
423: Section~\ref{sec:preliminaries} introduces the required notions and
424: \ifthenelse{\boolean{TR}}{%%
425: notations, including a minimal exposition of the main concepts of
426: abstract interpretation theory.
427: }{%%
428: notations.
429: }%%\ifthenelse{\boolean{TR}}{%%
430: Section~\ref{sec:analysis-of-computer-programs}
431: demonstrates the use of polyhedral computations in the specification
432: of a linear invariant analysis for
433: \ifthenelse{\boolean{TR}}{%%
434: a simple imperative language;
435: a few of the many applications for the analysis of computer programs
436: are briefly recalled.
437: }{%%
438: a simple imperative language.
439: }%%\ifthenelse{\boolean{TR}}{%%
440: Section~\ref{sec:analysis-of-hybrid-systems}
441: is devoted to polyhedral approximation techniques for hybrid systems,
442: which, as shown in Section~\ref{sec:analysis-of-analog-systems} can also
443: be applied to purely analog systems.
444: Section~\ref{sec:families-of-polyhedral-approximations}
445: presents several families of
446: \ifthenelse{\boolean{TR}}{%%
447: polyhedral approximations that provide a range of different
448: solutions to the complexity/precision trade-off.
449: }{%%
450: polyhedral approximations.
451: }%%\ifthenelse{\boolean{TR}}{%%
452: The most important operations that such approximations must provide
453: \ifthenelse{\boolean{TR}}{%%
454: in order to support analysis and verification methods
455: }{}%%\ifthenelse{\boolean{TR}}{%%
456: are illustrated in Section~\ref{sec:peculiar-polyhedral-computations}.
457: Section~\ref{sec:conclusion} concludes.
458:
459: \section{Preliminaries}
460: \label{sec:preliminaries}
461:
462: We assume some basic knowledge about lattice theory~\cite{Birkhoff67}.
463: Let $(S, \sqsseq)$ and $(T, \preceq)$ be two partially ordered sets;
464: the function $\fund{f}{S}{T}$ is \emph{monotonic} if,
465: for all $x_0, x_1 \in S$, $x_0 \sqsseq x_1$ implies $f(x_0) \preceq f(x_1)$.
466: If $(S, \sqsseq) \equiv (T, \preceq)$, so that $\fund{f}{S}{S}$,
467: an element $x \in S$ such that $x = f(x)$ is a \emph{fixpoint} of $f$.
468: If $(S, \sqsseq, \bot, \top, \sqcup, \sqcap)$ is a complete lattice,
469: then $f$ is \emph{continuous} if it preserves
470: the least upper bound of all increasing chains, i.e., for all
471: $x_0 \sqsseq x_1 \sqsseq \cdots$ in $S$, it satisfies
472: $f\bigl( \bigsqcup x_i \bigr) = \bigsqcup f(x_i)$;
473: in such a case, the least fixpoint of $f$ with respect to
474: the partial order `$\mathord{\sqsseq}$', denoted $\lfp f$, can be obtained
475: by iterating the application of $f$
476: starting from the bottom element $\bot$,
477: thereby computing the upward iteration sequence
478: \ifthenelse{\boolean{TR}}{%%
479: \[
480: \bot = f^0(\bot)
481: \sqsseq f^1(\bot)
482: \sqsseq f^2(\bot)
483: \sqsseq \cdots
484: \sqsseq f^i(\bot)
485: \sqsseq \cdots,
486: \]
487: up to the first non-zero limit ordinal $\omega$;
488: namely,
489: \[
490: \lfp f
491: = f^\omega(\bot)
492: \defeq
493: \bigsqcup_{i < \omega} f^i(\bot).
494: \]
495: }{%%
496: \(
497: \bot = f^0(\bot)
498: \sqsseq f^1(\bot)
499: \sqsseq f^2(\bot)
500: \sqsseq \cdots
501: \sqsseq f^i(\bot)
502: \sqsseq \cdots
503: \),
504: up to the first non-zero limit ordinal $\omega$;
505: namely,
506: \(
507: \lfp f
508: = f^\omega(\bot)
509: \defeq
510: \bigsqcup_{i < \omega} f^i(\bot)
511: \).
512: }%%\ifthenelse{\boolean{TR}}{%%
513:
514: For each $\fund{f_0}{S_0}{T_0}$ and $\fund{f_1}{S_1}{T_1}$,
515: the function
516: $\fund{f_0[f_1]}{(S_0 \union S_1)}{(T_0 \union T_1)}$
517: is defined, for each $x \in S_0 \union S_1$,
518: \ifthenelse{\boolean{TR}}{%%
519: by
520: \[
521: \bigl(f_0[f_1]\bigr)(x)
522: \defeq
523: \begin{cases}
524: f_1(x), &\text{if $x \in S_1$;} \\
525: f_0(x), &\text{if $x \in S_0 \setminus S_1$.}
526: \end{cases}
527: \]
528: }{%%
529: so that
530: $f_0[f_1](x) = f_1(x)$, if $x \in S_1$, and
531: $f_0[f_1](x) = f_0(x)$, otherwise.
532: }%%\ifthenelse{\boolean{TR}}{%%
533:
534: For $n > 0$, we denote by $\vect{v} = (v_0, \ldots, v_{n-1}) \in \Rset^n$
535: an $n$-tuple (vector) of real numbers;
536: $\nonnegRset$ is the set of non-negative real numbers;
537: \(
538: \langle \vect{v}, \vect{w} \rangle
539: \)
540: denotes the scalar product of vectors $\vect{v},\vect{w} \in \Rset^n$;
541: the vector $\vect{0} \in \Rset^n$ has all components equal to zero.
542: We write $\vect{v} \mathop{::} \vect{w}$
543: to denote the \emph{tuple concatenation}
544: of $\vect{v} \in \Rset^n$ and $\vect{w} \in \Rset^m$,
545: so that $\vect{v} \mathop{::} \vect{w} \in \Rset^{n+m}$.
546:
547: Let $\vect{x}$ be an $n$-tuple of distinct variables. Then
548: $\beta = \bigl( \langle \vect{a}, \vect{x} \rangle \relop b \bigr)$
549: denotes a linear inequality constraint,
550: for each vector $\vect{a} \in \Rset^n$, where $\vect{a} \neq \vect{0}$,
551: each scalar $b \in \Rset$, and
552: $\mathord{\relop} \in \{ \mathord{\geq}, \mathord{>} \}$.
553: A linear inequality constraint $\beta$ defines
554: a (topologically closed or open) affine half-space of $\Rset^n$,
555: denoted by $\con\bigl(\{\beta\}\bigr)$.
556:
557: A set $\cP \sseq \Rset^n$ is a \emph{(convex) polyhedron}
558: if and only if $\cP$ can be expressed as the intersection of
559: a finite number of affine half-spaces of $\Rset^n$, i.e.,
560: as the solution $\cP = \con(\cC)$
561: of a finite set of linear inequality constraints $\cC$
562: (called a \emph{constraint system}).
563: The set of all polyhedra on the vector space $\Rset^n$ is
564: denoted as $\Pset_n$. When partially ordered by set-inclusion,
565: convex polyhedra form a lattice
566: \(
567: (\Pset_n, \sseq, \emptyset, \Rset^n, \polyhull, \inters)
568: \)
569: having the empty set and $\Rset^n$ as the bottom
570: and top elements, respectively;
571: the binary meet operation, returning the greatest polyhedron
572: smaller than or equal to the two arguments, is easily seen
573: to correspond to set-intersection;
574: the binary join operation, returning the least polyhedron
575: greater than or equal to the two arguments,
576: is denoted `$\mathord{\polyhull}$' and called
577: \emph{convex polyhedral hull} (poly-hull, for short).
578: In general, the poly-hull of two polyhedra is different
579: from their convex hull~\cite{StoerW70}.
580:
581: A relation $\reld{\psi}{\Rset^n}{\Rset^n}$ (of dimension $n$)
582: is said to be \emph{affine} if there exists $\ell \in \Nset$ and
583: $\vect{a}_i, \vect{c}_i \in \Rset^n$,
584: $b_i \in \Rset$ and
585: $\mathord{\relop}_i \in \{ \geq, > \}$,
586: for each $i = 1, \ldots, \ell$,
587: such that
588: \begin{equation*}
589: \forall \vect{v}, \vect{w} \in \Rset^n
590: \itc
591: (\vect{v}, \vect{w}) \in \psi
592: \iff
593: \bigland_{i=1}^{\ell}
594: \bigl(
595: \langle \vect{c}_i, \vect{w} \rangle
596: \relop_i
597: \langle \vect{a}_i, \vect{v} \rangle + b_i
598: \bigr).
599: \end{equation*}
600: Any affine relation of dimension $n$ can thus be encoded by
601: $\ell$ linear inequalities on a $2n$-tuple of distinct variables
602: $\vect{x} \mathop{::} \vect{x}'$
603: (playing the role of $\vect{v}$ and $\vect{w}$, respectively),
604: therefore defining a polyhedron in $\Pset_{2n}$.
605: The set of polyhedra $\Pset_n$ is closed under the
606: (direct or inverse) application of affine relations:
607: i.e., for each $\cP \in \Pset_n$
608: and each affine relation $\reld{\psi}{\Rset^n}{\Rset^n}$,
609: the image $\psi(\cP)$ and the preimage $\psi^{-1}(\cP)$
610: are in $\Pset_n$.
611:
612: \subsection{Abstract Interpretation}
613: \label{sec:abstract-interpretation}
614:
615: The semantics of a hardware or software system is a mathematical
616: description of all its possible run-time behaviors. Different
617: semantics can be defined for the same system, depending on the
618: details being recorded. \emph{Abstract interpretation}
619: \ifthenelse{\boolean{TR}}{%%
620: \cite{CousotC77,CousotC79,CousotC92fr}
621: }{%%
622: \cite{CousotC79,CousotC92fr}
623: }%%\ifthenelse{\boolean{TR}}
624: is a formal method for relating these semantics according to their
625: level of abstraction, so that questions about the behavior of
626: a system can be provided with sound, possibly approximate answers.
627:
628: The concrete semantics $c \in C$ of a program is usually formalized as
629: the least fixpoint of a continuous semantic function $\fund{\cF}{C}{C}$,
630: where the concrete domain
631: $(C, \sqsseq, \bot, \top, \sqcup, \sqcap)$
632: is a complete lattice of semantic properties;
633: in many interesting cases, the computational order `$\sqsseq$' corresponds
634: to the approximation relation, so that $c_1 \sqsseq c_2$ holds
635: if $c_1$ is a stronger property than $c_2$
636: (i.e., $c_2$ correctly approximates $c_1$).
637:
638: For instance, the run-time behavior of a program may be defined in
639: terms of a transition system $\langle \Sigma, t, \iota \rangle$, where
640: $\Sigma$ is a set of states, $\iota \sseq \Sigma$ is the subset of initial
641: states, and $t \in \wp(\Sigma \times \Sigma)$ is a binary transition
642: relation mapping a state to its possible successor states.
643: Letting $\Sigma^\star$ denote
644: the set of all finite sequences of elements in $\Sigma$,
645: the initial history of a forward computation can be recorded%%
646: \TRfootnote{This is just one of a wide range of possible semantics;
647: by the same approach, other semantics may be described and related
648: by abstract interpretation~\cite{CousotC92fr}.}
649: as a partial execution trace
650: $\tau = \sigma_0 \cdots \sigma_m \in \Sigma^\star$
651: starting from an initial state $\sigma_0 \in \iota$
652: and such that any two consecutive states
653: $\sigma_i$ and $\sigma_{i+1}$ are related by the
654: transition relation, i.e., $(\sigma_i, \sigma_{i+1}) \in t$.
655: In such a context, an element of the concrete domain
656: \(
657: \bigl(
658: \wp(\Sigma^\star), \sseq, \emptyset, \Sigma^\star, \union, \inters
659: \bigr)
660: \)
661: is a set of partial execution traces and
662: the concrete semantics is $\lfp(\cF)$,
663: where the semantic function is defined by
664: \begin{multline*}
665: \cF
666: = \lambda X \in \wp(\Sigma^\star)
667: \lambdadot
668: X
669: \union
670: \{\,
671: \tau \in \Sigma^\star
672: \mid
673: \tau = \sigma_0 \in \iota
674: \,\} \\
675: \union
676: \bigl\{\,
677: \tau \sigma_{i+1} \in \Sigma^\star
678: \bigm|
679: \tau = \sigma_0 \cdots \sigma_i \in X,
680: (\sigma_i, \sigma_{i+1}) \in t
681: \,\bigr\}.
682: \end{multline*}
683: %%
684: An abstract domain\footnote{To avoid notational burden,
685: we will freely overload the lattice-theoretic symbols
686: `$\sqsseq$', `$\bot$', `$\sqcup$', etc.,
687: exploiting context to disambiguate their meaning.}
688: $(D^\sharp, \sqsseq, \bot, \sqcup)$
689: can be often modeled as a bounded join-semilattice,
690: so that it has a bottom element $\bot$
691: and the least upper bound
692: $d^\sharp_1 \sqcup d^\sharp_2$ exists
693: for all $d^\sharp_1, d^\sharp_2 \in D^\sharp$.
694: This domain is related to the concrete domain by a monotonic and injective
695: concretization function $\fund{\gamma}{D^\sharp}{C}$.
696: Monotonicity and injectivity mean that the abstract partial order
697: is equivalent to the approximation relation induced on $D^\sharp$
698: by the concretization function $\gamma$.
699: Conversely, the concrete domain is related to the abstract one
700: by a partial abstraction function $\pard{\alpha}{C}{D^\sharp}$ such that,
701: for each $c \in C$, if $\alpha(c)$ is defined then
702: $c \sqsubseteq \gamma\bigl(\alpha(c)\bigr)$.
703: In particular, we assume that $\alpha(\bot) = \bot$ is always defined;
704: when needed or useful, we will require a few additional properties.
705:
706: For example, a first abstraction of the semantics above,
707: typically adopted for the inference of
708: invariance properties of programs~\cite{CousotC79,CousotC92fr}, approximates
709: a set of traces by the set of states occurring in any one of the traces.
710: The \emph{reachable states} are thus characterized by elements of
711: the complete lattice
712: $\bigl( \wp(\Sigma), \sseq, \emptyset, \Sigma, \union, \inters \bigr)$,
713: which plays here the role of the abstract domain.
714: The concretization function relating $D^\sharp = \wp(\Sigma)$
715: to $C = \wp(\Sigma^\star)$ is defined, for each $d^\sharp \in \wp(\Sigma)$, by
716: \ifthenelse{\boolean{TR}}{%%
717: \[
718: }{%%
719: \(
720: }%%\ifthenelse{\boolean{TR}}{%%
721: \gamma(d^\sharp)
722: \defeq
723: \{\,
724: \tau \in \Sigma^\star
725: \mid
726: \tau = \sigma_0 \cdots \sigma_m,
727: \forall i = 0, \ldots, m \itc \sigma_i \in d^\sharp
728: \,\}.
729: \ifthenelse{\boolean{TR}}{%%
730: \]
731: }{%%
732: \)
733: }%%\ifthenelse{\boolean{TR}}{%%
734: The concrete semantic function
735: $\fund{\cF}{\wp(\Sigma^\star)}{\wp(\Sigma^\star)}$
736: can thus be approximated by the monotonic abstract semantic function
737: $\fund{\cA}{\wp(\Sigma)}{\wp(\Sigma)}$
738: defined by
739: \[
740: \cA
741: = \lambda d^\sharp \in \wp(\Sigma)
742: \lambdadot
743: d^\sharp
744: \union
745: \iota
746: \union
747: \bigl\{\,
748: \sigma' \in \Sigma
749: \bigm|
750: \exists \sigma \in d^\sharp \st (\sigma, \sigma') \in t
751: \,\bigr\}.
752: \]
753: This abstract semantic function is \emph{sound} with respect to
754: the concrete semantic function in that it satisfies the
755: local correctness requirement
756: \begin{equation*}
757: \label{eq:local-correctness-condition}
758: \forall c \in C
759: \itc
760: \forall d^\sharp \in D^\sharp
761: \itc
762: c \sqsseq \gamma(d^\sharp)
763: \implies
764: \cF(c) \sqsseq \gamma\bigl( \cA(d^\sharp) \bigr),
765: \end{equation*}
766: ensuring that each iteration $\cF^i(\bot)$
767: in the concrete fixpoint computation
768: is approximated by computing
769: the corresponding abstract iteration $\cA^i\bigl( \alpha(\bot) \bigr)$.
770: In particular, the least fixpoint of $\cF$ is approximated by
771: any post-fixpoint of~$\cA$
772: \ifthenelse{\boolean{TR}}{%%
773: \cite{CousotC77,CousotC92fr},
774: }{%%
775: \cite{CousotC92fr},
776: }%%\ifthenelse{\boolean{TR}}
777: i.e., any abstract element $d^\sharp \in D^\sharp$
778: such that $\cA(d^\sharp) \sqsseq d^\sharp$.
779:
780: Actually, the abstraction defined above satisfies an even
781: stronger property, in that the abstract semantic function $\cA$ is
782: the \emph{most precise} of all the sound approximations of $\cF$
783: that could be defined on the considered abstract domain.
784: This happens because the two domains are related by a
785: Galois connection~\cite{CousotC79}, i.e.,
786: there exists a total abstraction function
787: $\fund{\alpha}{C}{D^\sharp}$ satisfying
788: \[
789: \forall c \in C
790: \itc
791: \forall d^\sharp \in D^\sharp
792: \itc
793: \alpha(c) \sqsseq d^\sharp
794: \iff
795: c \sqsseq \gamma(d^\sharp).
796: \]
797: Namely,
798: \ifthenelse{\boolean{TR}}{%%
799: for all $c \in \wp(\Sigma^\star)$, we can define
800: \[
801: \alpha(c)
802: \defeq
803: \bigl\{\,
804: \sigma_i \in \Sigma
805: \bigm|
806: \tau = \sigma_0 \cdots \sigma_m \in c,
807: i \in \{0, \ldots, m\}
808: \,\bigr\}.
809: \]
810: }{%%
811: \(
812: \alpha(c)
813: \defeq
814: \bigl\{\,
815: \sigma_i \in \Sigma
816: \bigm|
817: \tau = \sigma_0 \cdots \sigma_m \in c,
818: i \in \{0, \ldots, m\}
819: \,\bigr\}
820: \).
821: }%%\ifthenelse{\boolean{TR}}{%%
822:
823: For Galois connections it can be shown
824: that $\alpha(c)$ is the best possible approximation in $D^\sharp$
825: for the concrete element $c \in C$;
826: similarly, $\alpha \compose \cF \compose \gamma$
827: (i.e., the function $\cA$ defined above)
828: is the best possible approximation for $\cF$
829: \cite{CousotC79}.
830: Such a result is provided with a quite intuitive reading;
831: in order to approximate the concrete function $\cF$
832: on an abstract element $d^\sharp \in D^\sharp$:
833: we first apply the concretization function $\gamma$ so as to obtain
834: the meaning of $d^\sharp$; then we apply the concrete function $\cF$;
835: finally, we abstract the result so as to obtain back an element of $D^\sharp$.
836:
837: Abstract interpretation theory can thus be used to specify (semi-)
838: automatic program analysis tools that are correct by design.
839: Of course ---due to well-known undecidability results---
840: any fully automatic tool can only provide partial, though safe answers.
841:
842: \subsection{Abstract Domains for Numeric and Boolean Values}
843: \label{sec:basic-abstract-domains}
844:
845: The reachable state abstraction described above is just one of the
846: possible semantic approximations that can be adopted when specifying
847: an abstract semantics. A further, typical approximation concerns the
848: description of the states of the transition system. Each state
849: $\sigma \in \Sigma$ may be decomposed into, e.g., a set of numerical or
850: Boolean variables that are of interest for the application at hand;
851: new abstract domains can be defined (and composed~\cite{CousotC79}) so
852: as to soundly describe the possible values of these variables.
853:
854: \ifthenelse{\boolean{TR}}{%%
855: As an expository example that will be also used in the following sections,
856: }{%%
857: As an expository example,
858: }%%\ifthenelse{\boolean{TR}}
859: assume that part of a state is characterized by
860: the value of an integer variable.
861: Then, the domain
862: $\bigl( \wp(\Sigma), \sseq, \emptyset, \Sigma, \union, \inters \bigr)$
863: can be abstracted to the concrete domain of integers
864: \(
865: \bigl(\wp(\Int), \sseq, \emptyset, \Int, \union, \inters\bigr)
866: \).
867: This domain is further approximated by an abstract domain
868: \(
869: \bigl(\Int^\sharp, \sqsubseteq, \bot, \sqcup\bigr)
870: \),
871: via the concretization function
872: $\fund{\gamma_\mathrm{I}}{\Int^\sharp}{\wp(\Int)}$.
873: Elements of $\Int^\sharp$ are denoted by $m^\sharp$,
874: possibly subscripted.
875: %%
876: We assume that the partial abstraction function
877: $\pard{\alpha_\mathrm{I}}{\wp(\Int)}{\Int^\sharp}$ is defined
878: on all singletons $\{m\} \in \wp(\Int)$ and on the whole set $\Int$.
879: We also assume that there are abstract binary operations
880: `$\absplus$', `$\absminus$' and `$\absprod$'
881: on $\Int^\sharp$ that are sound with respect to the corresponding
882: operations on $\wp(\Int)$ which, in turn, are the obvious pointwise
883: extensions of addition, subtraction and multiplication over the integers.
884: %%
885: More formally, for `$\absplus$'
886: we require
887: \(
888: \gamma_\mathrm{I}(m^\sharp_0 \absplus m^\sharp_1)
889: \supseteq
890: \bigl\{\,
891: m_0 + m_1
892: \bigm|
893: m_0 \in \gamma_\mathrm{I}(m^\sharp_0),
894: m_1 \in \gamma_\mathrm{I}(m^\sharp_1)
895: \,\bigr\}
896: \)
897: for each $m^\sharp_0, m^\sharp_1 \in \Int^\sharp$,
898: i.e., soundness with respect to addition.
899: Similar requirements are imposed on `$\absminus$' and `$\absprod$'.
900: Even though the definition of $\Int^\sharp$ is completely general,
901: families of integer intervals come naturally to mind for this role.
902:
903: Suppose now that some other part of the state is characterized by
904: the value of a Boolean expression.
905: Then, the domain
906: $\bigl( \wp(\Sigma), \sseq, \emptyset, \Sigma, \union, \inters \bigr)$
907: can be abstracted to the finite domain
908: \(
909: \bigl(
910: \wp(\Bool), \sseq, \emptyset, \Bool, \union, \inters
911: \bigr)
912: \),
913: where $\Bool = \{ \ffv, \ttv \}$ is the set of Boolean values.
914: In general, such a finite domain may be further approximated by
915: an abstract domain
916: \(
917: (\Bool^\sharp, \sqsseq, \bot, \top, \sqcup, \sqcap)
918: \),
919: related to the concrete domain by a Galois connection.
920: Elements of $\Bool^\sharp$ are denoted by $t^\sharp$, possibly subscripted,
921: and we can define abstract operations
922: `$\absneg$', `$\absor$' and `$\absand$' on $\Bool^\sharp$
923: that are sound with respect to the pointwise extensions
924: of Boolean negation, disjunction and conjunction over $\wp(\Bool)$.
925: %%
926: For instance, for the operation `$\absor$' to be sound with respect
927: to disjunction on $\wp(\Bool)$, it is required that,
928: \(
929: \gamma_\mathrm{B}(t^\sharp_0 \absor t^\sharp_1)
930: \supseteq
931: \bigl\{\,
932: t_0 \lor t_1
933: \bigm|
934: t_0 \in \gamma_\mathrm{B}(t^\sharp_0),
935: t_1 \in \gamma_\mathrm{B}(t^\sharp_1)
936: \,\bigr\}
937: \)
938: for each $t^\sharp_0$ and $t^\sharp_1$ in $\Bool^\sharp$.
939: Likewise for `$\absand$'.
940: For `$\absneg$' the correctness requirement is that,
941: for each $t^\sharp$ in $\Bool^\sharp$,
942: \(
943: \gamma_\mathrm{B}(\absneg t^\sharp)
944: \supseteq
945: \bigl\{\,
946: \neg t
947: \bigm|
948: t \in \gamma_\mathrm{B}(t^\sharp)
949: \,\bigr\}
950: \).
951: Abstract comparison operations
952: $\fund{\abseq,\abslt}{\Int^\sharp\times\Int^\sharp}{\Bool^\sharp}$
953: can then be defined to correctly approximate the equal-to and less-than
954: tests:
955: for each $m^\sharp_0, m^\sharp_1 \in \Int^\sharp$,
956: \(
957: \gamma_\mathrm{B}(m^\sharp_0 \abseq m^\sharp_1)
958: \supseteq
959: \bigl\{\,
960: m_0 = m_1
961: \bigm|
962: m_0 \in \gamma_\mathrm{I}(m^\sharp_0),
963: m_1 \in \gamma_\mathrm{I}(m^\sharp_1)
964: \,\bigr\}
965: \);
966: likewise for `$\abslt$'.
967:
968: Simple abstract domains such as the ones above can be combined in different
969: ways so as to obtain quite accurate approximations~\cite{CousotC79}.
970: In some cases, however, the required precision level may only be obtained
971: by a suitable initial choice of the abstract domain.
972: As a notable example, suppose that some part of the state $\sigma \in \Sigma$
973: is characterized by $n$ (integer or real valued) numeric variables and
974: the application at hand needs some \emph{relational} information about
975: these variables. In such a context, an approximation based on a simple
976: conjunctive combination of $n$ copies of the domain $\Int^\sharp$
977: described above will be almost useless. Rather, a new approximation
978: scheme can be devised by modeling states using the domain
979: \(
980: \bigl(
981: \wp(\Rset^n), \sseq, \emptyset, \Rset^n, \union, \inters
982: \bigr)
983: \),
984: where each vector $\vect{v} \in \Rset^n$ is meant to describe a possible
985: valuation for the $n$ variables. A further abstraction should map this
986: domain so as to retain some of the relations holding between the values
987: of the $n$ variables.
988: If a finite set of linear inequalities provides a good enough approximation,
989: then the natural choice is to abstract this domain
990: into the abstract domain of convex polyhedra
991: \(
992: (\Pset_n, \sseq, \emptyset, \Rset^n, \polyhull, \inters)
993: \)
994: \cite{CousotH78}.
995: In this case, the concrete and abstract domains are not related
996: by a Galois connection and, hence, a best approximation might not exist.%%
997: \footnote{This happens, for instance, when approximating an $n$-dimensional
998: ball with a convex polyhedron.}
999: Nonetheless, the convex polyhedral hull (partial) abstraction function
1000: $\pard{\polyhull}{\wp(\Rset^n)}{\Pset_n}$
1001: is defined in most of the cases of interest
1002: and provides the best possible approximation.
1003: Most of the arithmetic operations seen before can be encoded
1004: (or approximated) by computing images of affine relations.
1005:
1006: \subsection{Widening Operators}
1007:
1008: It should be stressed that, in general, the abstract semantics
1009: just described is not finitely computable. For instance,
1010: both the domain of convex polyhedra and the domain of integer intervals
1011: have infinite ascending chains, so that the limit of a converging
1012: fixpoint computation cannot generally be reached in a finite number
1013: of iterations.
1014:
1015: A finite computation can be enforced by further approximations
1016: resulting in a \emph{Noetherian} abstract domain,
1017: i.e., a domain where all ascending chains are finite.
1018: Alternatively, and more generally, it is possible
1019: to keep an abstract domain with infinite chains, while enforcing
1020: that these chains are traversed in a finite number of
1021: \ifthenelse{\boolean{TR}}{%%
1022: iteration steps \cite{CousotC92plilp}.
1023: }{%%
1024: iteration steps.
1025: }%%\ifthenelse{\boolean{TR}}{%%
1026: In both cases, termination is usually achieved to the detriment
1027: of precision, so that an appropriate trade-off should be pursued.
1028: \emph{Widening operators}
1029: \ifthenelse{\boolean{TR}}{%%
1030: \cite{CousotC76,CousotC77,CousotC92fr,CousotC92plilp}
1031: }{%%
1032: \cite{CousotC76,CousotC92fr}
1033: }%\ifthenelse{\boolean{TR}}
1034: provide a simple and general characterization for the second option.
1035:
1036: \begin{definition}
1037: \label{def:widening-operator}
1038: The partial operator $\pard{\widen}{D^\sharp \times D^\sharp}{D^\sharp}$
1039: is a \emph{widening} if:
1040: \begin{enumerate}
1041: \item
1042: for all $d^\sharp, e^\sharp \in D^\sharp$,
1043: $d^\sharp \sqsubseteq e^\sharp$ implies that
1044: $d^\sharp \widen e^\sharp$ is defined and
1045: $e^\sharp \sqsubseteq d^\sharp \widen e^\sharp$;
1046: \item
1047: for all increasing chains
1048: $e^\sharp_0 \sqsubseteq e^\sharp_1 \sqsubseteq \cdots$,
1049: the increasing chain defined by
1050: $d^\sharp_0 \defeq e^\sharp_0$ and
1051: \(
1052: d^\sharp_{i+1}
1053: \defeq
1054: d^\sharp_i \widen (d^\sharp_i \sqcup e^\sharp_{i+1})
1055: \),
1056: for $i \in \Nset$, is not strictly increasing.
1057: \end{enumerate}
1058: \end{definition}
1059:
1060: It can be proved that,
1061: for any monotonic operator $\fund{\cA}{D^\sharp}{D^\sharp}$,
1062: the upward iteration sequence with widenings
1063: starting at the bottom element $d^\sharp_0 \defeq \bot$
1064: and defined by
1065: \begin{equation*}
1066: d^\sharp_{i+1}
1067: \defeq
1068: \begin{cases}
1069: d^\sharp_i,
1070: &\text{if $\cA(d^\sharp_i) \sqsubseteq d^\sharp_i$,} \\
1071: d^\sharp_i
1072: \widen
1073: \bigl(d^\sharp_i \sqcup \cA(d^\sharp_i)\bigr),
1074: &\text{otherwise,}
1075: \end{cases}
1076: \end{equation*}
1077: converges to a post-fixpoint of $\mathord{\cA}$
1078: \ifthenelse{\boolean{TR}}{%%
1079: after a finite number of iterations \cite{CousotC92plilp}.
1080: }{%%
1081: after a finite number of iterations.
1082: }%%\ifthenelse{\boolean{TR}}{%%
1083: Clearly, the choice of the widening has a deep impact on the precision
1084: of the results obtained. Designing a widening which is appropriate
1085: for a given application is therefore a difficult (but possibly rewarding)
1086: activity.
1087:
1088:
1089: \section{Analysis and Verification of Computer Programs}
1090: \label{sec:analysis-of-computer-programs}
1091:
1092: In this section we begin a review of the applications of polyhedral
1093: computations to analysis and verification problems starting with the
1094: \ifthenelse{\boolean{TR}}{%%
1095: the work of Cousot and Halbwachs \cite{CousotH78,Halbwachs79th}.
1096: These seminal papers
1097: }{%%
1098: the work of Cousot and Halbwachs \cite{CousotH78}.
1099: This seminal paper
1100: }%% \ifthenelse{\boolean{TR}}
1101: on the automatic inference of linear invariants for
1102: imperative programs constituted a major leap forward for at least two reasons.
1103: First, the polyhedral domain proposed by Cousot and Halbwachs
1104: was considerably more powerful than all the data-flow analyses known
1105: at that time, including the rather sophisticated one by Karr
1106: \ifthenelse{\boolean{TR}}{%%
1107: which was limited to linear equalities \cite{Karr76,Muller-OlmS04ICALP}.
1108: }{%%
1109: which was limited to linear equalities \cite{Karr76}.
1110: }%% \ifthenelse{\boolean{TR}}
1111: Secondly, the use of convex polyhedra as an abstract domain established
1112: abstract interpretation as the right methodology for the definition
1113: of complex and correct program analyzers.
1114:
1115: We illustrate the basic ideas by partially specifying the analysis
1116: of linear invariants for a very simple imperative language.
1117: The simplicity of the language we have chosen for expository purposes
1118: should not mislead the reader: the approach is generalizable to any
1119: imperative (and, for that matter, functional and logic) language
1120: \cite{BagnaraHPZ07TR}.
1121: The abstract syntax of the language is presented in
1122: Figure~\ref{fig:IMP-syntax}.
1123: \begin{figure}
1124: \ifthenelse{\boolean{TR}}{%%
1125: \begin{description}
1126: \item[Integers]
1127: $m \in \Int \defeq \Zset$
1128: \item[Booleans]
1129: $t \in \Bool \defeq \{ \ttv, \ffv \}$
1130: \item[Variables]
1131: $x \in \Var \defeq \{ x_0, x_1, x_2, \ldots \}$
1132: \end{description}
1133: \begin{description}
1134: \item[Arithmetic expressions]
1135: \[
1136: \Aexp \ni
1137: a ::= m \vbar x \vbar a_0 + a_1 \vbar a_0 - a_1 \vbar a_0 * a_1
1138: \]
1139: \item[Boolean expressions]
1140: \[
1141: \Bexp \ni
1142: b ::= t \vbar a_0 = a_1 \vbar a_0 < a_1
1143: \]
1144: \item[Statements]
1145: \begin{align*}
1146: \Stmt \ni
1147: s ::= \kw{skip} \vbar x := a \vbar s_0 ; s_1
1148: \vbar \kw{if} b \kw{then} s_0 \kw{else} s_1
1149: \vbar \kw{while} b \kw{do} s
1150: \end{align*}
1151: \end{description}
1152: }{%%
1153: \begin{gather*}
1154: m \in \Int \defeq \Zset
1155: \qquad
1156: t \in \Bool \defeq \{ \ttv, \ffv \}
1157: \qquad
1158: x \in \Var \defeq \{ x_0, x_1, x_2, \ldots \} \\
1159: \begin{aligned}
1160: \Aexp \ni
1161: a &::= m \vbar x \vbar a_0 + a_1 \vbar a_0 - a_1 \vbar a_0 * a_1 \\
1162: \Bexp \ni
1163: b &::= t \vbar a_0 = a_1 \vbar a_0 < a_1 \\
1164: \Stmt \ni
1165: s &::= \kw{skip} \vbar x := a \vbar s_0 ; s_1
1166: \vbar \kw{if} b \kw{then} s_0 \kw{else} s_1
1167: \vbar \kw{while} b \kw{do} s
1168: \end{aligned}
1169: \end{gather*}
1170: }%% \ifthenelse{\boolean{TR}}{%%
1171: \caption{Abstract syntax of the simple imperative language}
1172: \label{fig:IMP-syntax}
1173: \end{figure}
1174: The basic syntactic categories, corresponding to the sets $\Int$, $\Bool$
1175: and $\Var$, are defined directly.
1176: From these, the categories of arithmetic and Boolean expressions
1177: and of statements are defined by means of BNF rules.
1178: Notice the use of syntactic meta-variables: for instance,
1179: to save typing we will consistently denote by $s$, possibly subscripted
1180: or superscripted, any element of $\Stmt$.
1181:
1182: The concrete semantics of programs is formally defined using the
1183: \emph{natural semantics} approach \cite{Kahn87}.
1184: This, in turn, is a ``big-step'' operational semantics defined by structural
1185: induction on program structures in the style of Plotkin \cite{Plotkin81}.
1186: First we define the notion of \emph{store}, which is any mapping
1187: between a finite set of variables and elements of $\Int$.
1188: Formally, a store is an element of the set
1189: \ifthenelse{\boolean{TR}}{%%
1190: \[
1191: }{%%
1192: \(
1193: }%%\ifthenelse{\boolean{TR}}
1194: \Store
1195: \defeq
1196: \{\,
1197: \fund{\sigma}{V}{\Int}
1198: \mid
1199: V \sseq \Var, \,\text{$V$ finite}
1200: \,\}
1201: \ifthenelse{\boolean{TR}}{%%
1202: \]
1203: }{%%
1204: \)
1205: }%%\ifthenelse{\boolean{TR}}
1206: and denoted by the letter $\sigma$,
1207: possibly subscripted or superscripted.
1208: The store obtained from $\sigma \in \Store$ by the assignment
1209: of $m \in \Int$ to $x \in \dom(\sigma)$, denoted by $\sigma[m/x]$,
1210: \ifthenelse{\boolean{TR}}{%%
1211: is defined as follows, for each $x' \in \dom(\sigma)$:%
1212: \[
1213: \sigma[m/x](x')
1214: \defeq
1215: \begin{cases}
1216: m, &\text{if $x' = x$;} \\
1217: \sigma(x'), &\text{if $x' \neq x$.}
1218: \end{cases}
1219: \]
1220: }{%%
1221: is defined so that,
1222: for each $x' \in \dom(\sigma)$,
1223: $\sigma[m/x](x') = m$, if $x' = x$, and
1224: $\sigma[m/x](x') = \sigma(x')$, otherwise.
1225: }%%\ifthenelse{\boolean{TR}}{%%
1226:
1227: The concrete evaluation relations that complete the definition of the
1228: concrete semantics for our simple language are defined by structural
1229: induction from a set of rule schemata.
1230: The evaluation relations for terminating computations are given by
1231: $\reld{\aceval}{(\Aexp \times \Store)}{\Int}$,
1232: for arithmetic expressions,
1233: $\reld{\bceval}{(\Bexp \times \Store)}{\Bool}$,
1234: for Boolean expressions, and
1235: $\reld{\sceval}{(\Stmt \times \Store)}{\Store}$,
1236: for statements.
1237: The judgment $\langle a, \sigma \rangle \aceval m$ means that
1238: when expression $a$ is executed in store $\sigma$ it results in
1239: the integer $m$.
1240: The judgment $\langle b, \sigma \rangle \bceval t$ is
1241: similar. Note that expressions do not have, in our simple language,
1242: side effects.
1243: The judgment $\langle s, \sigma \rangle \sceval \sigma'$ means that
1244: the statement $s$, executed in store $\sigma$, results in a (possibly
1245: modified) store $\sigma'$.
1246: The rule schemata, in the form $\frac{\text{premise}}{\text{conclusion}}$,
1247: that define these relations are given
1248: in Figure~\ref{fig:IMP-concrete-semantics}.
1249: \begin{figure}
1250: \begin{gather*}
1251: \prooftree
1252: \nohyp
1253: \justifies
1254: \langle m, \sigma \rangle
1255: \aceval
1256: m
1257: \endprooftree
1258: \quad\hfill
1259: \prooftree
1260: \nohyp
1261: \justifies
1262: \langle x, \sigma \rangle
1263: \aceval
1264: \sigma(x)
1265: \endprooftree
1266: \quad\hfill
1267: \prooftree
1268: \langle a_0, \sigma \rangle
1269: \aceval
1270: m_0
1271: \quad
1272: \langle a_1, \sigma \rangle
1273: \aceval
1274: m_1
1275: \justifies
1276: \langle a_0 + a_1, \sigma \rangle
1277: \aceval
1278: m_0 + m_1
1279: \endprooftree \\[2ex]
1280: \prooftree
1281: \langle a_0, \sigma \rangle
1282: \aceval
1283: m_0
1284: \quad
1285: \langle a_1, \sigma \rangle
1286: \aceval
1287: m_1
1288: \justifies
1289: \langle a_0 - a_1, \sigma \rangle
1290: \aceval
1291: m_0 - m_1
1292: \endprooftree
1293: \quad
1294: \prooftree
1295: \langle a_0, \sigma \rangle
1296: \aceval
1297: m_0
1298: \quad
1299: \langle a_1, \sigma \rangle
1300: \aceval
1301: m_1
1302: \justifies
1303: \langle a_0 * a_1, \sigma \rangle
1304: \aceval
1305: m_0 \cdot m_1
1306: \endprooftree \\[2ex]
1307: \prooftree
1308: \langle a_0, \sigma \rangle
1309: \aceval
1310: m_0
1311: \quad
1312: \langle a_1, \sigma \rangle
1313: \aceval
1314: m_1
1315: \justifies
1316: \langle a_0 = a_1, \sigma \rangle
1317: \bceval
1318: (m_0 = m_1)
1319: \endprooftree
1320: \quad
1321: \prooftree
1322: \langle a_0, \sigma \rangle
1323: \aceval
1324: m_0
1325: \quad
1326: \langle a_1, \sigma \rangle
1327: \aceval
1328: m_1
1329: \justifies
1330: \langle a_0 < a_1, \sigma \rangle
1331: \bceval
1332: (m_0 < m_1)
1333: \endprooftree \\[2ex]
1334: \prooftree
1335: \nohyp
1336: \justifies
1337: \langle \kw{skip}, \sigma \rangle
1338: \sceval
1339: \sigma
1340: \endprooftree
1341: \quad
1342: \prooftree
1343: \langle a, \sigma \rangle
1344: \aceval
1345: m
1346: \justifies
1347: \langle x := a, \sigma \rangle
1348: \sceval
1349: \sigma[m/x]
1350: \endprooftree
1351: \quad
1352: \prooftree
1353: \langle s_0, \sigma \rangle
1354: \sceval
1355: \sigma''
1356: \quad
1357: \langle s_1, \sigma'' \rangle
1358: \sceval
1359: \sigma'
1360: \justifies
1361: \langle s_0 ; s_1, \sigma \rangle
1362: \sceval
1363: \sigma'
1364: \endprooftree \\[2ex]
1365: \prooftree
1366: \langle b, \sigma \rangle
1367: \bceval
1368: \ttv
1369: \quad
1370: \langle s_0, \sigma \rangle
1371: \sceval
1372: \sigma'
1373: \justifies
1374: \langle \kw{if} b \kw{then} s_0 \kw{else} s_1, \sigma \rangle
1375: \sceval
1376: \sigma'
1377: \endprooftree
1378: \qquad\qquad\qquad
1379: \prooftree
1380: \langle b, \sigma \rangle
1381: \bceval
1382: \ffv
1383: \quad
1384: \langle s_1, \sigma \rangle
1385: \sceval
1386: \sigma'
1387: \justifies
1388: \langle \kw{if} b \kw{then} s_0 \kw{else} s_1, \sigma \rangle
1389: \sceval
1390: \sigma'
1391: \endprooftree \\[2ex]
1392: \prooftree
1393: \langle b, \sigma \rangle
1394: \bceval
1395: \ffv
1396: \justifies
1397: \langle \kw{while} b \kw{do} c, \sigma \rangle
1398: \sceval
1399: \sigma
1400: \endprooftree
1401: \quad
1402: \prooftree
1403: \langle b, \sigma \rangle
1404: \bceval
1405: \ttv
1406: \quad
1407: \langle c, \sigma \rangle
1408: \sceval
1409: \sigma''
1410: \quad
1411: \langle \kw{while} b \kw{do} c, \sigma'' \rangle
1412: \sceval
1413: \sigma'
1414: \justifies
1415: \langle \kw{while} b \kw{do} c, \sigma \rangle
1416: \sceval
1417: \sigma'
1418: \endprooftree
1419: \end{gather*}
1420: \caption{Concrete semantics rule schemata for the finite computations
1421: of the simple imperative language}
1422: \label{fig:IMP-concrete-semantics}
1423: \end{figure}
1424: Rule instances can be composed in the obvious way to form finite
1425: tree structures, representing finite computations.
1426: \ifthenelse{\boolean{TR}}{%%
1427: Figure~\ref{fig:example-of-concrete-tree} shows one such tree.
1428:
1429: \begin{sidewaysfigure}
1430: \[
1431: \prooftree
1432: \prooftree
1433: \prooftree
1434: \nohyp
1435: \justifies
1436: \langle 0, \sigma_0 \rangle \aceval 0
1437: \endprooftree
1438: %\;
1439: \prooftree
1440: \nohyp
1441: \justifies
1442: \langle x_0, \sigma_0 \rangle \aceval 1
1443: \endprooftree
1444: \justifies
1445: \langle 0 < x_0, \sigma_0 \rangle
1446: \bceval
1447: \ttv
1448: \endprooftree
1449: %\;
1450: \prooftree
1451: \prooftree
1452: \prooftree
1453: \prooftree
1454: \nohyp
1455: \justifies
1456: \langle x_1, \sigma_0 \rangle
1457: \aceval
1458: 1
1459: \endprooftree
1460: %\;
1461: \prooftree
1462: \nohyp
1463: \justifies
1464: \langle 2, \sigma_0 \rangle
1465: \aceval
1466: 2
1467: \endprooftree
1468: \justifies
1469: \langle x_1+2, \sigma_0 \rangle
1470: \aceval
1471: 3
1472: \endprooftree
1473: \justifies
1474: \langle x_1 := x_1+2, \sigma_0 \rangle
1475: \sceval
1476: \sigma_1
1477: \endprooftree
1478: %\;
1479: \prooftree
1480: \prooftree
1481: \prooftree
1482: \nohyp
1483: \justifies
1484: \langle x_0, \sigma_1 \rangle
1485: \aceval
1486: 1
1487: \endprooftree
1488: %\;
1489: \prooftree
1490: \nohyp
1491: \justifies
1492: \langle x_1, \sigma_1 \rangle
1493: \aceval
1494: 3
1495: \endprooftree
1496: \justifies
1497: \langle x_0-x_1, \sigma_1 \rangle
1498: \aceval
1499: -2
1500: \endprooftree
1501: \justifies
1502: \langle x_0 := x_0-x_1, \sigma_1 \rangle
1503: \sceval
1504: \sigma_2
1505: \endprooftree
1506: \justifies
1507: \bigl\langle (x_1 := x_1+2; x_0 := x_0-x_1), \sigma_0 \bigr\rangle
1508: \sceval
1509: \sigma_2
1510: \endprooftree
1511: %\;
1512: \prooftree
1513: \prooftree
1514: \prooftree
1515: \nohyp
1516: \justifies
1517: \langle 0, \sigma_2 \rangle \aceval 0
1518: \endprooftree
1519: %\;
1520: \prooftree
1521: \nohyp
1522: \justifies
1523: \langle x_0, \sigma_2 \rangle \aceval -2
1524: \endprooftree
1525: \justifies
1526: \langle 0 < x_0, \sigma_2 \rangle
1527: \bceval
1528: \ffv
1529: \endprooftree
1530: \justifies
1531: \langle w, \sigma_2 \rangle
1532: \sceval
1533: \sigma_2
1534: \endprooftree
1535: \justifies
1536: \bigl\langle
1537: \kw{while}\, 0 < x_0\, \kw{do}\, (x_1 := x_1+2; x_0 := x_0-x_1),
1538: \sigma_0
1539: \bigr\rangle
1540: \sceval
1541: \sigma_2
1542: \endprooftree
1543: \]
1544:
1545: \medskip
1546: \noindent
1547: Legend:
1548: \begin{align*}
1549: \sigma_0 &\defeq \bigl\{ (x_0, 1), (x_1, 1) \bigr\}, \\
1550: \sigma_1 &\defeq \bigl\{ (x_0, 1), (x_1, 3) \bigr\}, \\
1551: \sigma_2 &\defeq \bigl\{ (x_0, -2), (x_1, 3) \bigr\}, \\
1552: w &\defeq \bigl(\kw{while}\, 0 < x_0\, \kw{do}\, (x_1 := x_1+2; x_0 := x_0-x_1)\bigr).
1553: \end{align*}
1554: \caption{The tree representing a concrete execution of a program}
1555: \label{fig:example-of-concrete-tree}
1556: \end{sidewaysfigure}
1557: }{}%%\ifthenelse{\boolean{TR}}
1558:
1559: The possibly infinite set of all finite trees is obtained by means
1560: of a least fixpoint computation, corresponding to the classical
1561: inductive interpretation of the rules
1562: in Figure~\ref{fig:IMP-concrete-semantics}.
1563: The rule schemata in Figure~\ref{fig:IMP-concrete-semantics-divergence}
1564: can be used to directly model non-terminating computations and need to
1565: \ifthenelse{\boolean{TR}}{%%
1566: be interpreted coinductively \cite{CousotC92,Leroy06,Schmidt98}.
1567: }{%%
1568: be interpreted coinductively \cite{CousotC92}.
1569: }%%\ifthenelse{\boolean{TR}}
1570: \begin{figure}
1571: \begin{gather*}
1572: \prooftree
1573: \langle s_0, \sigma \rangle
1574: \diverges
1575: \justifies
1576: \langle s_0 ; s_1, \sigma \rangle
1577: \diverges
1578: \endprooftree
1579: \qquad\qquad\qquad
1580: \prooftree
1581: \langle s_0, \sigma \rangle
1582: \sceval
1583: \sigma'
1584: \quad
1585: \langle s_1, \sigma' \rangle
1586: \diverges
1587: \justifies
1588: \langle s_0 ; s_1, \sigma \rangle
1589: \diverges
1590: \endprooftree \\[2ex]
1591: \prooftree
1592: \langle b, \sigma \rangle
1593: \bceval
1594: \ttv
1595: \quad
1596: \langle s_0, \sigma \rangle
1597: \diverges
1598: \justifies
1599: \langle \kw{if} b \kw{then} s_0 \kw{else} s_1, \sigma \rangle
1600: \diverges
1601: \endprooftree
1602: \qquad\qquad\qquad
1603: \prooftree
1604: \langle b, \sigma \rangle
1605: \bceval
1606: \ffv
1607: \quad
1608: \langle s_1, \sigma \rangle
1609: \diverges
1610: \justifies
1611: \langle \kw{if} b \kw{then} s_0 \kw{else} s_1, \sigma \rangle
1612: \diverges
1613: \endprooftree \\[2ex]
1614: \prooftree
1615: \langle b, \sigma \rangle
1616: \bceval
1617: \ttv
1618: \quad
1619: \langle c, \sigma \rangle
1620: \diverges
1621: \justifies
1622: \langle \kw{while} b \kw{do} c, \sigma \rangle
1623: \diverges
1624: \endprooftree
1625: \quad
1626: \prooftree
1627: \langle b, \sigma \rangle
1628: \bceval
1629: \ttv
1630: \quad
1631: \langle c, \sigma \rangle
1632: \sceval
1633: \sigma'
1634: \quad
1635: \langle \kw{while} b \kw{do} c, \sigma' \rangle
1636: \diverges
1637: \justifies
1638: \langle \kw{while} b \kw{do} c, \sigma \rangle
1639: \diverges
1640: \endprooftree
1641: \end{gather*}
1642: \caption{Additional concrete semantics rule schemata
1643: for the infinite computations of the simple imperative language}
1644: \label{fig:IMP-concrete-semantics-divergence}
1645: \end{figure}
1646: The judgment $\langle s, \sigma \rangle \diverges$ means that
1647: the statement $s$ diverges when executed in store $\sigma$.
1648: By a suitable adaptation of the computational ordering,
1649: both sets of finite and infinite trees can be jointly computed
1650: in a single least fixpoint computation
1651: \ifthenelse{\boolean{TR}}{%%
1652: \cite{CousotC92,Leroy06,Schmidt98}.
1653: }{%%
1654: \cite{CousotC92}.
1655: }%%\ifthenelse{\boolean{TR}}{%%
1656: While these semantics characterizations contain all the information we need
1657: to perform a wide range of program reasoning tasks, they are generally
1658: not computable: we have thus to resort to approximation.
1659:
1660: Following the abstract interpretation approach, as instantiated
1661: \ifthenelse{\boolean{TR}}{%%
1662: in \cite{Schmidt95,Schmidt97,Schmidt98},
1663: }{%%
1664: in \cite{Schmidt95},
1665: }%%\ifthenelse{\boolean{TR}}{%%
1666: the concrete rule schemata
1667: are paired with abstract rule schemata that correctly approximate them.
1668: Before doing that, we need to formalize abstract domains for each concrete
1669: domain used by the concrete semantics.
1670:
1671: For simple approximations of integers and Boolean expressions,
1672: we consider the abstract domains $\Int^\sharp$ and $\Bool^\sharp$
1673: introduced in Section~\ref{sec:basic-abstract-domains}.
1674: The last (and most interesting) abstraction we need is one that approximates
1675: sets of stores. We thus require an abstract domain
1676: \(
1677: \bigl(\Store^\sharp, \sqsubseteq, \bot, \sqcup \bigr)
1678: \)
1679: that is related, by means of a concretization function
1680: $\gamma_\mathrm{S}$ such that $\gamma_\mathrm{S}(\bot) = \emptyset$,
1681: to the concrete domain
1682: \(
1683: \bigl(\wp(\Store), \sseq, \emptyset, \Store, \union, \inters \bigr)
1684: \).
1685: Elements of $\Store^\sharp$ are denoted by
1686: $\sigma^\sharp$, possibly subscripted.
1687: The abstract store evaluation and update operators
1688: \begin{gather*}
1689: \fund{\cdot[\cdot]}%
1690: {(\Store^\sharp \times \Aexp)}%
1691: {\Int^\sharp}, \\
1692: \fund{\cdot[\cdot := \cdot]}%
1693: {\bigl(\Store^\sharp \times \Var \times \Aexp\bigr)}%
1694: {\Store^\sharp}, \\
1695: \fund{\cdot[\cdot / \cdot]}%
1696: {\bigl(\Store^\sharp \times \Var \times \Int^\sharp\bigr)}%
1697: {\Store^\sharp}
1698: \end{gather*}
1699: are assumed to be sound with respect to their concrete counterparts,
1700: i.e., such that,
1701: for each $\sigma^\sharp \in \Store^\sharp$, $a \in \Aexp$,
1702: $x \in \Var$ and $m^\sharp \in \Int^\sharp$:
1703: \begin{align*}
1704: \gamma_\mathrm{I}\bigl(\sigma^\sharp[a]\bigr)
1705: &\supseteq
1706: \bigl\{\,
1707: m \in \Int
1708: \bigm|
1709: \sigma \in \gamma_\mathrm{S}(\sigma^\sharp),
1710: \langle a, \sigma \rangle \aceval m
1711: \,\bigr\}, \\
1712: \gamma_\mathrm{S}\bigl(\sigma^\sharp\bigl[x := a]\bigr)
1713: &\supseteq
1714: \bigl\{\,
1715: \sigma' \in \Store
1716: \bigm|
1717: \sigma \in \gamma_\mathrm{S}(\sigma^\sharp),
1718: \langle x := a, \sigma \rangle \sceval \sigma'
1719: \,\bigr\}, \\
1720: \gamma_\mathrm{S}\bigl(\sigma^\sharp\bigl[m^\sharp/x]\bigr)
1721: &\supseteq
1722: \bigl\{\,
1723: \sigma[m/x] \in \Store
1724: \bigm|
1725: \sigma \in \gamma_\mathrm{S}(\sigma^\sharp),
1726: m \in \gamma_\mathrm{I}(m^\sharp)
1727: \,\bigr\}.
1728: \end{align*}
1729: We also need computable ``Boolean filters'' to refine the information
1730: contained in abstract stores, i.e., two functions
1731: $\fund{\phi_\ttv,\phi_\ffv}{\Store^\sharp \times \Bexp}{\Store^\sharp}$
1732: such that,
1733: \ifthenelse{\boolean{TR}}{%%
1734: for each $\sigma^\sharp \in \Store^\sharp$ and $b \in \Bexp$,
1735: \begin{align*}
1736: \gamma_\mathrm{S}\bigl(\phi_\ttv(\sigma^\sharp, b)\bigr)
1737: &\supseteq
1738: \bigl\{\,
1739: \sigma \in \gamma_\mathrm{S}(\sigma^\sharp)
1740: \bigm|
1741: \langle b, \sigma \rangle \bceval \ttv
1742: \,\bigr\}, \\
1743: \gamma_\mathrm{S}\bigl(\phi_\ffv(\sigma^\sharp, b)\bigr)
1744: &\supseteq
1745: \bigl\{\,
1746: \sigma \in \gamma_\mathrm{S}(\sigma^\sharp)
1747: \bigm|
1748: \langle b, \sigma \rangle \bceval \ffv
1749: \,\bigr\}.
1750: \end{align*}
1751: }{%%
1752: for each $t \in \Bool$, $\sigma^\sharp \in \Store^\sharp$ and $b \in \Bexp$:
1753: \[
1754: \gamma_\mathrm{S}\bigl(\phi_t(\sigma^\sharp, b)\bigr)
1755: \supseteq
1756: \bigl\{\,
1757: \sigma \in \gamma_\mathrm{S}(\sigma^\sharp)
1758: \bigm|
1759: \langle b, \sigma \rangle \bceval t
1760: \,\bigr\}.
1761: \]
1762: }%%\ifthenelse{\boolean{TR}}{%%
1763: %%
1764: We are now in a position to present,
1765: in Figure~\ref{fig:IMP-abstract-semantics},
1766: a possible set of domain-independent abstract rule schemata.
1767: \begin{figure}
1768: \begin{gather*}
1769: \prooftree
1770: \nohyp
1771: \justifies
1772: \langle m, \sigma^\sharp \rangle
1773: \aaeval
1774: \alpha_\mathrm{I}\bigl(\{m\}\bigr)
1775: \endprooftree
1776: \quad\hfill
1777: \prooftree
1778: \nohyp
1779: \justifies
1780: \langle x, \sigma^\sharp \rangle
1781: \aaeval
1782: \sigma^\sharp[x]
1783: \endprooftree
1784: \quad\hfill
1785: \prooftree
1786: \langle a_0, \sigma^\sharp \rangle
1787: \aaeval
1788: m^\sharp_0
1789: \quad
1790: \langle a_1, \sigma^\sharp \rangle
1791: \aaeval
1792: m^\sharp_1
1793: \justifies
1794: \langle a_0 + a_1, \sigma^\sharp \rangle
1795: \aaeval
1796: m^\sharp_0 \absplus m^\sharp_1
1797: \endprooftree \\[2ex]
1798: \prooftree
1799: \langle a_0, \sigma^\sharp \rangle
1800: \aaeval
1801: m^\sharp_0
1802: \quad
1803: \langle a_1, \sigma^\sharp \rangle
1804: \aaeval
1805: m^\sharp_1
1806: \justifies
1807: \langle a_0 - a_1, \sigma^\sharp \rangle
1808: \aaeval
1809: m^\sharp_0 \absminus m^\sharp_1
1810: \endprooftree
1811: \quad\hfill
1812: \prooftree
1813: \langle a_0, \sigma^\sharp \rangle
1814: \aaeval
1815: m^\sharp_0
1816: \quad
1817: \langle a_1, \sigma^\sharp \rangle
1818: \aaeval
1819: m^\sharp_1
1820: \justifies
1821: \langle a_0 * a_1, \sigma^\sharp \rangle
1822: \aaeval
1823: m^\sharp_0 \absprod m^\sharp_1
1824: \endprooftree \\[2ex]
1825: \prooftree
1826: \nohyp
1827: \justifies
1828: \langle t, \sigma^\sharp \rangle
1829: \baeval
1830: \alpha_\mathrm{B}\bigl(\{t\}\bigr)
1831: \endprooftree
1832: \quad\hfill
1833: \prooftree
1834: \langle a_0, \sigma^\sharp \rangle
1835: \aaeval
1836: m^\sharp_0
1837: \quad
1838: \langle a_1, \sigma^\sharp \rangle
1839: \aaeval
1840: m^\sharp_1
1841: \justifies
1842: \langle a_0 = a_1, \sigma^\sharp \rangle
1843: \baeval
1844: m^\sharp_0 \abseq m^\sharp_1
1845: \endprooftree \\[2ex]
1846: \prooftree
1847: \langle a_0, \sigma^\sharp \rangle
1848: \aaeval
1849: m^\sharp_0
1850: \quad
1851: \langle a_1, \sigma^\sharp \rangle
1852: \aaeval
1853: m^\sharp_1
1854: \justifies
1855: \langle a_0 < a_1, \sigma^\sharp \rangle
1856: \baeval
1857: m^\sharp_0 \abslt m^\sharp_1
1858: \endprooftree
1859: \quad\hfill
1860: \prooftree
1861: \nohyp
1862: \justifies
1863: \langle \kw{skip}, \sigma^\sharp \rangle
1864: \saeval
1865: \sigma^\sharp
1866: \endprooftree \\[2ex]
1867: \prooftree
1868: \langle a, \sigma^\sharp \rangle
1869: \aaeval
1870: m^\sharp
1871: \using\;\text{(i)}
1872: \justifies
1873: \langle x := a, \sigma^\sharp \rangle
1874: \saeval
1875: \sigma^\sharp[x := a]
1876: \endprooftree
1877: \quad\hfill
1878: \prooftree
1879: \langle a, \sigma^\sharp \rangle
1880: \aaeval
1881: m^\sharp
1882: \using\;\text{(ii)}
1883: \justifies
1884: \langle x := a, \sigma^\sharp \rangle
1885: \saeval
1886: \sigma^\sharp[m^\sharp/x]
1887: \endprooftree \\
1888: \prooftree
1889: \langle s_0, \sigma^\sharp_0 \rangle
1890: \saeval
1891: \sigma^\sharp_1
1892: \quad
1893: \langle s_1, \sigma^\sharp_1 \rangle
1894: \saeval
1895: \sigma^\sharp_2
1896: \justifies
1897: \langle s_0 ; s_1, \sigma^\sharp_0 \rangle
1898: \saeval
1899: \sigma^\sharp_2
1900: \endprooftree \\[2ex]
1901: \prooftree
1902: \langle b, \sigma^\sharp \rangle
1903: \baeval
1904: t^\sharp
1905: \quad
1906: \bigl\langle s_0, \phi_\ttv(\sigma^\sharp, b) \bigr\rangle
1907: \saeval
1908: \sigma^\sharp_0
1909: \quad
1910: \bigl\langle s_1, \phi_\ffv(\sigma^\sharp, b) \bigr\rangle
1911: \saeval
1912: \sigma^\sharp_1
1913: \justifies
1914: \langle \kw{if} b \kw{then} s_0 \kw{else} s_1, \sigma^\sharp \rangle
1915: \saeval
1916: \sigma^\sharp_0 \sqcup \sigma^\sharp_1
1917: \endprooftree \\[2ex]
1918: \prooftree
1919: \langle b, \sigma^\sharp \rangle
1920: \baeval
1921: t^\sharp
1922: \quad
1923: \bigl\langle c, \phi_\ttv(\sigma^\sharp, b) \bigr\rangle
1924: \saeval
1925: \sigma^\sharp_1
1926: \quad
1927: \langle \kw{while} b \kw{do} c, \sigma^\sharp_1 \rangle
1928: \saeval
1929: \sigma^\sharp_2
1930: \justifies
1931: \langle \kw{while} b \kw{do} c, \sigma^\sharp \rangle
1932: \saeval
1933: \phi_\ffv(\sigma^\sharp, b) \sqcup \sigma^\sharp_2
1934: \endprooftree
1935: \end{gather*}
1936:
1937: \begin{quote}
1938: {
1939: \footnotesize
1940: \begin{itemize}
1941: \item[Notes:]
1942: \item[(i)] This rule is used if the domain $\Store^\sharp$ can
1943: capture the assignment precisely (e.g., when
1944: $\Store^\sharp$ is a domain of convex polyhedra and $a$ is
1945: an affine expression). Notice that the premise is intentionally
1946: not used: its presence is required in order to ensure that the
1947: abstract tree approximates the concrete tree in its entirety.
1948: \item[(ii)] This rule is used when (i) is not applicable.
1949: \end{itemize}
1950: }
1951: \end{quote}
1952: \caption{Abstract semantics rule schemata for the simple imperative language}
1953: \label{fig:IMP-abstract-semantics}
1954: \end{figure}
1955: These schemata allow for the free approximation of the `$\rightsquigarrow$'
1956: right-hand sides in the conclusions. This means that if, e.g.,
1957: \ifthenelse{\boolean{TR}}{%%
1958: \[
1959: \prooftree
1960: \text{premise}
1961: \justifies
1962: \langle s, \sigma \rangle \saeval \sigma^\sharp_1
1963: \endprooftree
1964: \]
1965: is an instance of some rule, then
1966: \[
1967: \prooftree
1968: \text{premise}
1969: \justifies
1970: \langle s, \sigma \rangle \saeval \sigma^\sharp_2
1971: \endprooftree
1972: \]
1973: }{%%
1974: $\frac{\text{premise}}{\langle s, \sigma \rangle \saeval \sigma^\sharp_1}$
1975: is an instance of some rule, then
1976: $\frac{\text{premise}}{\langle s, \sigma \rangle \saeval \sigma^\sharp_2}$
1977: }%%\ifthenelse{\boolean{TR}}{%%
1978: is also an instance of the same rule for each $\sigma^\sharp_2$
1979: such that $\sigma^\sharp_1 \sqsseq \sigma^\sharp_2$.
1980: Hence the schemata in Figure~\ref{fig:IMP-abstract-semantics}
1981: ensure correctness yet leaving complete freedom about precision.
1982: The ability to give up some precision, as we will see, is crucial
1983: in order to ensure the (reasonably quick) termination of the analysis.
1984:
1985: It is possible to prove that,
1986: for each (possibly infinite) concrete tree $T$
1987: built using the schemata of Figures~\ref{fig:IMP-concrete-semantics}
1988: and~\ref{fig:IMP-concrete-semantics-divergence},
1989: for each (possibly infinite) abstract tree $T^\sharp$
1990: built using the schemata of Figure~\ref{fig:IMP-abstract-semantics},
1991: if the concrete tree root is of the form
1992: $\langle s, \sigma \rangle \sceval \sigma_1$
1993: (when the tree is finite)
1994: or $\langle s, \sigma \rangle \diverges$
1995: (when the tree is infinite)
1996: and the abstract tree root is of the form
1997: $\langle s, \sigma^\sharp \rangle \saeval \sigma^\sharp_1$ with
1998: $\sigma \in \gamma_\mathrm{S}(\sigma^\sharp)$,
1999: then $T^\sharp$ correctly approximates $T$.
2000: This means not only that $\sigma_1 \in \gamma_\mathrm{S}(\sigma^\sharp_1)$
2001: (when $T$ is finite), but also that \emph{each} node in $T$ is correctly
2002: approximated by at least one node in $T^\sharp$.
2003: In other words, the abstract tree correctly approximates the entire
2004: concrete computation (see \cite{BagnaraHPZ07TR} for the details).
2005:
2006: \ifthenelse{\boolean{TR}}{%%
2007: It is worth stressing the observation in~\cite{Schmidt98} that,
2008: }{%%
2009: It is worth stressing the observation by Schmidt that,
2010: }%%\ifthenelse{\boolean{TR}}{%%
2011: even when disregarding the non-terminating concrete computations,
2012: the abstract rules still have to be interpreted coinductively
2013: because most of the finite concrete trees can only be approximated
2014: by infinite abstract trees; for instance, all abstract trees containing
2015: a while loop are infinite.
2016: %%
2017: Since, in general, we cannot effectively compute infinite abstract trees,
2018: we still do not have a viable analysis technique. The solution is to restrict
2019: ourselves to the class of rational trees, i.e., trees with only finitely many
2020: subtrees and that, consequently, admit a finite representation.
2021:
2022: The analysis algorithm is sketched in \cite{Schmidt95}.
2023: For expository purposes, we describe here a simplified version that,
2024: however, is enough to handle the considered programming language
2025: features.
2026: The algorithm works by recursively constructing a finite approximation
2027: for the (possibly infinite) abstract subtree rooted in
2028: the current node (initially, the root of the whole tree).
2029: The current node
2030: $n = \bigl(\langle p, \sigma^\sharp_n \rangle \rightsquigarrow r_n\bigr)$,
2031: where $r_n$ is a placeholder for the ``yet to be computed'' conclusion,
2032: is processed according to the following alternatives:
2033: \begin{enumerate}
2034: \item
2035: \label{enum-case:expand}
2036: If no ancestor of $n$ has $p$ in the label, the node has to be
2037: expanded using an applicable abstract rule instance.
2038: Namely, descendants of the premises of the rule are (recursively)
2039: processed, one at a time and from left to right.
2040: When the expansion of all the premises has been completed, including
2041: the case when the rule has no premise at all, the marker $r_n$
2042: is replaced by an abstract value computed according to the conclusion
2043: of the rule.
2044: \item
2045: \label{enum-case:subsumed}
2046: If there exists an ancestor node
2047: $m = \langle p, \sigma^\sharp_m \rangle \rightsquigarrow r_m$ of $n$
2048: labeled by the same syntax $p$ and such that
2049: $\sigma^\sharp_n \sqsubseteq \sigma^\sharp_m$,
2050: i.e., if node $n$ is subsumed by node $m$,
2051: then the node is not expanded further and
2052: the placeholder $r_n$ is replaced by the least fixpoint of the equation
2053: $r_n = f_m(r_n)$, where $f_m$ is the expression corresponding to
2054: the conclusion of the abstract rule that was used for the expansion
2055: of node $m$.%
2056: \footnote{As explained in
2057: \ifthenelse{\boolean{TR}}{%%
2058: \cite{Schmidt95,Schmidt98},
2059: }{%%
2060: \cite{Schmidt95},
2061: }%%\ifthenelse{\boolean{TR}}{%%
2062: the computation of such a \emph{least} fixpoint
2063: (in the context of a coinductive interpretation of the abstract rules)
2064: is justified by the fact that here we only need to approximate
2065: the conclusions produced by the terminating concrete
2066: \ifthenelse{\boolean{TR}}{%%
2067: computations,
2068: i.e., by the concrete rules of Figure~\ref{fig:IMP-concrete-semantics},
2069: which are interpreted inductively. Also note that the divergence rules of
2070: Figure~\ref{fig:IMP-concrete-semantics-divergence} have no conclusion at all.
2071: }{%%
2072: computations.
2073: }%%\ifthenelse{\boolean{TR}}
2074: }
2075: \item
2076: \label{enum-case:widen}
2077: Otherwise, there must be an ancestor node
2078: $m = \langle p, \sigma^\sharp_m \rangle \rightsquigarrow r_m$ of $n$
2079: labeled by the same syntax $p$, but the subsumption condition
2080: $\sigma^\sharp_n \sqsubseteq \sigma^\sharp_m$ does not hold.
2081: Then there are two options:
2082: \begin{enumerate}
2083: \item
2084: \label{enum-case:widen-finite}
2085: if the abstract domain $\Store^\sharp$ is finite,
2086: we proceed as in case~(\ref{enum-case:expand});
2087: \item
2088: \label{enum-case:widen-infinite}
2089: if the abstract domain $\Store^\sharp$ is infinite,
2090: to ensure convergence,
2091: a widening `$\widen$' over $\Store^\sharp$ can be employed%
2092: \TRfootnote{If $\Store^\sharp$ is infinite but Noetherian,
2093: we can choose $\widen \defeq \sqcup$ as a widening.}
2094: and store $\sigma^\sharp_n$ in node $n$ is replaced by
2095: $\sigma^\sharp_m \widen (\sigma^\sharp_m \sqcup \sigma^\sharp_n)$.
2096: Then, we proceed again as in case~(\ref{enum-case:expand}).
2097: \end{enumerate}
2098: \end{enumerate}
2099:
2100: The abstract semantics of Figure~\ref{fig:IMP-abstract-semantics}
2101: and the given algorithm for computing a rational abstract tree are
2102: fully generic in that any choice for the abstract domains $\Int^\sharp$,
2103: $\Bool^\sharp$ and $\Store^\sharp$ will result into a provably
2104: correct analysis algorithm.
2105: Focusing on numerical domains, the role of $\Int^\sharp$ can be played
2106: by any domain of intervals, so that the operations
2107: `$\absplus$', `$\absminus$' and `$\absprod$' are the standard
2108: ones of interval arithmetic~\cite{AlefeldH83};
2109: for instance,
2110: \(
2111: [m^\mathrm{l}_0, m^\mathrm{u}_0] \absplus [m^\mathrm{l}_1,m^\mathrm{u}_1]
2112: \defeq
2113: [m^\mathrm{l}_0+m^\mathrm{l}_1, m^\mathrm{u}_0+m^\mathrm{u}_1]
2114: \).
2115: More sophisticated domains, such as \emph{modulo intervals}
2116: \cite{NakanishiJPF99}, are able to encode more precise information
2117: about the set of \emph{integer} values each variable can take.
2118: For $\Store^\sharp$, a common choice is to abstract from the integrality
2119: of variables and consider a domain of convex polyhedra which, in exchange,
2120: allows the tracking of relational information.
2121: With reference to Figure~\ref{fig:IMP-abstract-semantics},
2122: rule (i) can be applied directly when the arithmetic expression
2123: $a = \langle \vect{a}, \vect{x} \rangle + b$ is affine;
2124: the corresponding polyhedral operation is
2125: the computation of the image of a polyhedron
2126: by a special case of affine relation $\reld{\psi}{\Rset^n}{\Rset^n}$,
2127: called \emph{single-update affine function}:
2128: \[
2129: (\vect{v}, \vect{w}) \in \psi
2130: \iff
2131: w_k = \langle \vect{a}, \vect{v} \rangle + b
2132: \land
2133: \bigland_{\genfrac{}{}{0pt}{}{\scriptstyle 0 \leq i < n}{\scriptstyle i \neq k}}
2134: w_i = v_i.
2135: \]
2136: Another special case, slightly more general than the one above and called
2137: \emph{single-update bounded affine relation}, allows among other things
2138: to approximate nonlinear assignments and to realize rule (ii).
2139: For fixed vectors $\vect{a}, \vect{c} \in \Rset^n$
2140: and scalars $b, d \in \Rset$:
2141: \[
2142: (\vect{v}, \vect{w}) \in \psi
2143: \iff
2144: \langle \vect{a}, \vect{v} \rangle + b
2145: \leq w_k
2146: \leq \langle \vect{c}, \vect{v} \rangle + d
2147: \land
2148: \bigland_{\genfrac{}{}{0pt}{}{\scriptstyle 0 \leq i < n}{\scriptstyle i \neq k}}
2149: w_i = v_i.
2150: \]
2151: Both the rules for the if-then-else and the while constructs
2152: require the Boolean filters and least upper bound operations:
2153: these are realized by means of intersections (or the addition
2154: of individual constraints) and poly-hulls, respectively.
2155: These, together with the containment test used to detect the reaching
2156: of post-fixpoints and the widening
2157: (see Section~\ref{sec:peculiar-polyhedral-computations})
2158: used to ensure termination of the analysis algorithm,
2159: are all the operations required for the analysis
2160: of our simple imperative language. More complex languages
2161: require other operations: for instance, the analysis of languages with
2162: command blocks needs to have the possibility of embedding polyhedra into
2163: a space of higher dimension, reorganizing the dimensions, and projecting
2164: polyhedra on spaces of lower dimension. Other operations are needed
2165: to accommodate different semantic constructions (e.g., affine preimages
2166: for backward semantics), to allow for the efficient modeling of data objects
2167: (e.g., summarized dimensions to approximate the values of unbounded
2168: collections \cite{GopanRS05}), and to help scalability
2169: (e.g., simplifications of polyhedra \cite{Frehse05}).
2170:
2171: \ifthenelse{\boolean{TR}}{%%
2172: Figure~\ref{fig:example-of-abstract-tree} illustrates
2173: an abstract computation that, by following the analysis algorithm above,
2174: approximates the concrete tree in Figure~\ref{fig:example-of-concrete-tree}:
2175: intervals and polyhedra approximate
2176: sets of integers and sets of stores, respectively.
2177: \begin{sidewaysfigure}
2178: \begin{gather*}
2179: \prooftree
2180: \prooftree
2181: \prooftree
2182: \nohyp
2183: \justifies
2184: \langle 0, \cQ_0 \rangle \aaeval [0,0]
2185: \endprooftree
2186: %\;
2187: \prooftree
2188: \nohyp
2189: \justifies
2190: \langle x_0, \cQ_0 \rangle \aaeval \top
2191: \endprooftree
2192: \justifies
2193: \langle 0 < x_0, \cQ_0 \rangle
2194: \baeval
2195: \top
2196: \endprooftree
2197: %\;
2198: \prooftree
2199: \prooftree
2200: \omissis
2201: \justifies
2202: \langle x_1 := x_1+2, \cQ_0^t \rangle
2203: \saeval
2204: \cQ_0'
2205: \endprooftree \text{(i)}
2206: \;
2207: \prooftree
2208: \omissis
2209: \justifies
2210: \langle x_0 := x_0-x_1, \cQ_0' \rangle
2211: \saeval
2212: \cQ_1
2213: \endprooftree \text{(i)}
2214: \justifies
2215: \bigl\langle (x_1 := x_1+2;\, x_0 := x_0-x_1), \cQ_0^t \bigr\rangle
2216: \saeval
2217: \cQ_1
2218: \endprooftree
2219: %\;
2220: \prooftree
2221: \nohyp
2222: \justifies
2223: \langle w, \cQ_1 \rangle
2224: \saeval
2225: \cQ \dblue{\mathord{} = \cQ_0^f}
2226: \endprooftree \text{(\ref{enum-case:subsumed})}
2227: \justifies
2228: \langle w, \cQ_0 \rangle
2229: \saeval
2230: \cP = (\cQ_0^f \polyhull \cQ) \dblue{\mathord{} = \cQ_0^f}
2231: \black{\text{ (\ref{enum-case:subsumed})}}
2232: \endprooftree \\[4mm]
2233: \prooftree
2234: \prooftree
2235: \prooftree
2236: \nohyp
2237: \justifies
2238: \langle 0, \cP_0 \rangle \aaeval [0,0]
2239: \endprooftree
2240: %\;
2241: \prooftree
2242: \nohyp
2243: \justifies
2244: \langle x_0, \cP_0 \rangle \aaeval [1,\infty]
2245: \endprooftree
2246: \justifies
2247: \langle 0 < x_0, \cP_0 \rangle
2248: \baeval
2249: \alpha_\mathrm{B}\bigl(\{\ttv\}\bigr)
2250: \endprooftree
2251: %\;
2252: \prooftree
2253: \prooftree
2254: \omissis
2255: \justifies
2256: \langle x_1 := x_1+2, \cP_0^t \rangle
2257: \saeval
2258: \cP_0'
2259: \endprooftree \text{(i)}
2260: \;
2261: \prooftree
2262: \omissis
2263: \justifies
2264: \langle x_0 := x_0-x_1, \cP_0' \rangle
2265: \saeval
2266: \cP_1
2267: \endprooftree \text{(i)}
2268: \justifies
2269: \bigl\langle (x_1 := x_1+2;\, x_0 := x_0-x_1), \cP_0^t \bigr\rangle
2270: \saeval
2271: \cP_1
2272: \endprooftree
2273: %\;
2274: \langle w, \cP_1 \rangle
2275: \saeval
2276: \cP
2277: \black{\text{ (\ref{enum-case:widen-infinite})}}
2278: \justifies
2279: \langle w, \cP_0 \rangle
2280: \saeval
2281: (\cP_0^f \polyhull \cP) = (\emptyset \polyhull \cP) = \cP
2282: \endprooftree
2283: \end{gather*}
2284:
2285: \medskip
2286: \noindent
2287: Legend:
2288: \begin{align*}
2289: w
2290: &\defeq
2291: \bigl(
2292: \kw{while}\, 0 < x_0\, \kw{do}\, (x_1 := x_1+2;\, x_0 := x_0-x_1)
2293: \bigr), \\
2294: \cP_0 &\defeq \con\bigl(\{x_0 \geq 1, x_1 = 1\}\bigr), \quad
2295: &\cQ_0 &\defeq \cP_0 \widen (\cP_0 \polyhull \cP_1)
2296: =\con\bigl(\{2 x_0 + 3 x_1 \geq 5, x_1 \geq 1\}\bigr), \\
2297: \cP_0^t &\defeq \phi_\ttv(\cP_0, 0 < x_0)
2298: = \cP_0, \quad
2299: & \cQ_0^t &\defeq \phi_\ttv(\cQ_0, 0 < x_0)
2300: = \con\bigl(\{x_0 \geq 1, x_1 \geq 1\}\bigr), \\
2301: \cP_0^f &\defeq \phi_\ffv(\cP_0, 0 < x_0)
2302: = \emptyset, \quad
2303: &\cQ_0^f &\defeq \phi_\ffv(\cQ_0, 0 < x_0)
2304: = \con\bigl(\{2 x_0 + 3 x_1 \geq 5, x_0 \leq 0\}\bigr), \\
2305: \cP_0' &\defeq \con\bigl(\{x_0 \geq 1, x_1 = 3\}\bigr), \quad
2306: &\cQ_0' &\defeq \con\bigl(\{x_0 \geq 1, x_1 \geq 3\}\bigr), \\
2307: \cP_1 &\defeq \con\bigl(\{x_0 \geq -2, x_1 = 3\}\bigr), \quad
2308: &\cQ_1 &\defeq \con\bigl(\{x_0 + x_1 \geq 1, x_1 \geq 3\}\bigr).
2309: \end{align*}
2310: Notes:
2311: \begin{itemize}
2312: \item[(i)]
2313: Rule (i) of Figure~\ref{fig:IMP-abstract-semantics} is used here.
2314: \item[(\ref{enum-case:subsumed})]
2315: Case (\ref{enum-case:subsumed}) of the algorithm is applied here.
2316: \item[(\ref{enum-case:widen-infinite})]
2317: Case (\ref{enum-case:widen-infinite}) of the algorithm is applied here.
2318: \end{itemize}
2319: \caption{Finite approximation of an infinite abstract computation tree}
2320: \label{fig:example-of-abstract-tree}
2321: \end{sidewaysfigure}
2322: The initial abstract store is given by the polyhedron
2323: $\cP_0 = \con\bigl(\{x_0 \geq 1, x_1 = 1\}\bigr)$,
2324: which approximates all concrete stores $\sigma$ satisfying
2325: $\sigma(x_0) \geq 1$ and $\sigma(x_1) = 1$ including
2326: the concrete store $\sigma_0$ in~Figure~\ref{fig:example-of-concrete-tree}.
2327: %
2328: Consider first the lower tree in~Figure~\ref{fig:example-of-concrete-tree}.
2329: This corresponds to the stage in the computation when
2330: all possible instances of case~(\ref{enum-case:expand}) of the algorithm
2331: have been applied.
2332: In particular, the two leftmost subtrees are derived according
2333: to the abstract semantics rules in Figure~\ref{fig:IMP-abstract-semantics}
2334: by only using case~(\ref{enum-case:expand}) of the algorithm.
2335: For the rightmost child which has still to be expanded,
2336: $\cP$ is a placeholder for its conclusion.
2337: It is also noted that, in the root of this tree,
2338: since $\cP_0^f = \emptyset$, the final result will be
2339: the same as the value assigned to $\cP$.
2340: Since the rightmost child,
2341: satisfies the conditions of case~(\ref{enum-case:widen-infinite})
2342: of the algorithm, the abstract store $\cP_1$ must undergo a
2343: widening computation, yielding the abstract store $\cQ_0$.
2344: Thus this node has to be replaced by
2345: $\langle w, \cQ_0 \rangle \saeval \cP$.
2346: %
2347: Consider now the upper tree in~Figure~\ref{fig:example-of-concrete-tree}
2348: which has the root $\langle w, \cQ_0 \rangle \saeval \cP$ as above.
2349: The two left-most immediate subtrees
2350: are derived, as in the lower tree,
2351: by only using case~(\ref{enum-case:expand}) of the algorithm.
2352: The rightmost child is initially given $\cQ$ as a placeholder
2353: for its conclusion.
2354: Since this node
2355: satisfies the conditions for case~(\ref{enum-case:subsumed})
2356: of the algorithm, it is not expanded further;
2357: and the value of $\cQ$ is obtained by finding the least fixpoint solution
2358: for the equation
2359: $\cQ = \cQ_0^f \polyhull \cQ$;
2360: namely,
2361: $\cQ_0^f = \con\bigl(\{2 x_0 + 3 x_1 \geq 5, x_0 \leq 0\}\bigr)$.
2362: Thus in the conclusion of the root of the upper tree we have
2363: $\cP = \cQ_0^f \polyhull \cQ = \cQ_0^f$.
2364: %
2365: Finally, the completed abstract tree can be obtained by
2366: replacing the rightmost child of the lower tree by the upper tree
2367: and the placeholder $\cP$ in the conclusion of the root
2368: of the lower tree by $\cQ_0^f$.
2369: }{}%%\ifthenelse{\boolean{TR}}
2370:
2371: Based on suitable variations of the simple linear invariant analysis
2372: outlined in this section (possibly combined with other analyses),
2373: many different applications have been proposed in the literature.
2374: %%
2375: Examples include the absence of common run-time arithmetic errors,
2376: such as floating-point exceptions, overflows and divisions by zero
2377: \cite{BlanchetCCFMMMR03};
2378: the absence of out-of-bounds array indexing~\cite{CousotH78,VenetB04},
2379: as well as other buffer overruns caused by
2380: incorrect string manipulations~\cite{DorRS01,Ellenbogen04th};
2381: the analysis of programs manipulating (possibly unbounded)
2382: heap-allocated data structures, so as to prove the absence
2383: of several kinds of pointer errors (e.g., memory leaks)
2384: \cite{GopanRS05,ShahamKS00};
2385: the computation of input/output argument size relations
2386: \ifthenelse{\boolean{TR}}{%%
2387: in logic programs~\cite{BenoyK97,GobertLC07,HenriksenG06};
2388: }{%%
2389: in logic programs~\cite{BenoyK97};
2390: }%%\ifthenelse{\boolean{TR}}{%%
2391: the detection of potential security vulnerabilities in x86 binaries
2392: that allow to bypass intrusion detection systems~\cite{KruegelKMRV05};
2393: the inference of temporal schedulability constraints that a partially
2394: specified set of real-time tasks has to satisfy~\cite{DooseM05}.
2395: %%
2396: All of the above are examples of \emph{safety} properties, whereby a
2397: computer program is proved to be free from some undesired behavior.
2398: However, the computation of invariant linear relations is also
2399: an important, often indispensable step when aiming at proving
2400: \emph{progress} properties,
2401: such as termination~\cite{Cousot05,MesnardB05TPLP,SohnVG91}.
2402: %%
2403: It should be also stressed that the same approach, after some minor
2404: adaptations, can be applied to the analysis of alternative computation
2405: paradigms such as, e.g.,
2406: \emph{gated data dependence graphs}~\cite{HymansU04}
2407: (an intermediate representation for compilers)
2408: and \emph{batch workflow networks}~\cite{vanHeeOSV06}
2409: (a form of Petri net used in workflow management).
2410:
2411:
2412: \section{Analysis and Verification of Hybrid Systems}
2413: \label{sec:analysis-of-hybrid-systems}
2414:
2415: Hybrid systems (that is, dynamical systems with both continuous
2416: and discrete components)
2417: are commonly modeled by hybrid automata~\cite{AlurCHH93,Frehse05,Henzinger96}.
2418: These, often highly complex, systems are usually nonlinear (making
2419: them computationally intractable as they are).
2420: However, linear approximations, which allow the use of polyhedral computations
2421: for the model checking operations, have been used successfully for
2422: the verification of useful safety properties
2423: \ifthenelse{\boolean{TR}}{%%
2424: \cite{DoyenHR05,Frehse04,Frehse05,FrehseHK04,SankaranarayananSM06,SongCR06}.
2425: }{%%
2426: \cite{DoyenHR05,Frehse05,SongCR06}.
2427: }%\ifthenelse{\boolean{TR}}
2428:
2429: \ifthenelse{\boolean{TR}}{%%
2430: In this section, we illustrate, by means of examples, how polyhedral
2431: computations can be used for verifying simple properties of hybrid automata.
2432: The examples are all instances of \emph{linear hybrid systems}, a
2433: particular class of hybrid systems that can be modeled using polyhedra
2434: where the continuous behavior is specified
2435: by linear constraints over the time-derivatives of the variables.
2436: }{}
2437: \begin{definition}
2438: \summary{(Linear hybrid automaton.)}
2439: \label{def:linear-hybrid-automaton}
2440: A \emph{linear hybrid automaton} (of dimension $n$)
2441: is a tuple
2442: \ifthenelse{\boolean{TR}}{%%
2443: \[
2444: (\Loc, \Init, \Act, \Inv, \Lab, \Trans)
2445: \]
2446: }{%%
2447: $(\Loc, \Init, \Act, \Inv, \Lab, \Trans)$
2448: }%%\ifthenelse{\boolean{TR}}
2449: where the first component
2450: $\Loc$ is a finite set of \emph{locations}.
2451: The functions
2452: $\fund{\Init}{\Loc}{\Pset_n}$, $\fund{\Act}{\Loc}{\Pset_n}$
2453: and $\fund{\Inv}{\Loc}{\Pset_n}$ define polyhedra. In particular,
2454: for each location $\ell \in \Loc$:
2455: $\Init(\ell)$ specifies the set of possible
2456: initial values the $n$ variables can take if the automaton
2457: starts at $\ell$;
2458: $\Act(\ell)$ specifies the possible derivative values of the $n$ variables,
2459: so that, if the automaton reaches $\ell$ with values
2460: given by the vector $\vect{v}$,
2461: then after staying there for a delay of
2462: $t \in \nonnegRset$, the values will be given by a vector
2463: $\vect{v} + t\vect{w}$, where $\vect{w} \in \Act(\ell)$;
2464: $\Inv(\ell)$ specifies the values that an $n$-vector $\vect{v}$
2465: may have at $\ell$.
2466: The fifth and sixth components
2467: provide a set of \emph{synchronization labels} $\Lab$
2468: and a labeled set of affine transition relations
2469: $\reld{\Trans}{\Loc}{\Lab \times \Pset_{2n} \times \Loc}$,
2470: required to hold when moving from the \emph{source} location
2471: (the first argument)
2472: to the \emph{target} location (the fourth argument).
2473: \end{definition}
2474: Observe that the only differences between this definition of a
2475: linear hybrid automaton and those in, for
2476: \ifthenelse{\boolean{TR}}{%%
2477: example~\cite{AlurCHHHNOSY95,Frehse04,HalbwachsPR97,Henzinger96},
2478: }{%%
2479: example~\cite{HalbwachsPR97,Henzinger96},
2480: }%%\ifthenelse{\boolean{TR}}{%%
2481: are presentational; in particular, as we have used polyhedra to
2482: represent the linear constraints, there is no need to provide, as is
2483: the case in these other definitions, an explicit component of the
2484: system consisting of the set of $n$ variables.
2485:
2486: The synchronization labels $\Lab$ are required for specifying large
2487: systems. Each part of the system is specified by a separate automaton,
2488: and then \emph{parallel composition} is employed
2489: to combine the components into an automaton for the complete system.
2490: This ensures that communication between the automata occurs,
2491: via selected input/output variables,
2492: between transitions that have the same label.
2493: Example~\ref{ex:scheduler} provides a very simple
2494: illustration of parallel composition;
2495: formal definitions are available
2496: \ifthenelse{\boolean{TR}}{%%
2497: in~\cite{AlurCHH93,Henzinger96}
2498: and a larger application can be found in~\cite{MullerS00}.
2499: }{%%
2500: in~\cite{AlurCHH93,Henzinger96}.
2501: }%%\ifthenelse{\boolean{TR}}
2502:
2503: A linear hybrid automaton can be represented by a directed graph
2504: whose nodes are the locations and edges are the transitions
2505: from the source to the target locations.
2506: Each node $\ell$ is labeled by two sets of constraints defining
2507: the polyhedra $\Inv(\ell)$ and $\Act(\ell)$.
2508: To distinguish these constraints, if, for example $x$ is a variable
2509: used for the constraints defining $\Inv(\ell)$,
2510: $\dot{x}$ will be used in the constraints defining $\Act(\ell)$.%
2511: \footnote{The dot notation reflects the fact
2512: that these variables denote the derivatives of the state variables.}
2513: In the examples, the initial polyhedron $\Init(\ell)$
2514: is assumed to be empty unless there is an arrow
2515: to $\ell$ (with no source node) labeled by the constraint system
2516: defining $\Init(\ell)$.
2517: Each edge $\tau = \bigl(\ell, a, \cP, \ell') \in \Trans$,
2518: is labeled by a constraint system $\cC$ defining $\cP$ and, optionally,
2519: by $a$ which is only included
2520: where it is used for the parallel composition of automata.
2521: Since $\cP \in \Pset_{2n}$, we specify $\cC$ by using two $n$-tuples
2522: of variables $\vect{x}$ and $\vect{x}'$, which are interpreted as usual
2523: to denote the variables in the source $\ell$ and target $\ell'$ locations,
2524: respectively.
2525: We also adopt some helpful shorthand notation:
2526: $x\plusplus$ and $x\minusminus$ denote
2527: $x' = x + 1$ and $x' = x - 1$, respectively;
2528: also, constraints of the form $x' = x$ are omitted.
2529: The following examples, taken (with some minor modifications)
2530: from~\cite{AlurCHH93,HalbwachsPR97}, illustrate the automata.
2531: \begin{example}
2532: \label{ex:water-monitor}
2533: A graphical view of a water-level monitor automaton
2534: is given in \textup{Figure~\ref{fig:water-level-monitor}}.
2535: \begin{figure}[p]
2536: \centering
2537: {\scriptsize
2538: \begin{picture}(330,160)(0,-5)
2539: \put(0,0){
2540: \setlength{\unitlength}{0.7pt}%
2541: \psset{xunit=1cm,yunit=1cm,runit=1cm}
2542: \psset{origin={0,0}}
2543: \pspicture*[](-1,0)(10,10)
2544: \psline{->}(-0.5,3.75)(1,3.75)
2545: \rput(0,4){$w = 1$}
2546: \rput(0.75,3.2){$\ell_0$}
2547: \psframe[framearc=.3](1,3)(2.5,4.5)
2548: \rput(1.7,4.2){$w < 10$}
2549: \rput(1.7,3.8){$\dot{x} = 1$}
2550: \rput(1.7,3.4){$\dot{w} = 1$}
2551: \rput(4.5,4){$w = 10, x' = 0$}
2552: \psline{->}(2.5,3.75)(6.5,3.75)
2553: \rput(4.5,3.5){signal pump off}
2554: \rput(8.3,3.2){$\ell_1$}
2555: \psframe[framearc=.3](6.5,3)(8,4.5)
2556: \rput(7.2,4.2){$x < 2$}
2557: \rput(7.2,3.8){$\dot{x} = 1$}
2558: \rput(7.2,3.4){$\dot{w} = 1$}
2559: \rput(6.5,2.3){switch off}
2560: \psline{->}(7.25,3)(7.25,1.5)
2561: \rput(7.75,2.3){$x = 2$}
2562: \rput(8.3,0.2){$\ell_2$}
2563: \psframe[framearc=.3](6.5,0)(8,1.5)
2564: \rput(7.2,1.2){$w > 5$}
2565: \rput(7.2,0.8){$\dot{x} = 1$}
2566: \rput(7.2,0.4){$\dot{w} = -2$}
2567: \rput(4.5,1){$w = 5, x' = 0$}
2568: \psline{<-}(2.5,0.75)(6.5,0.75)
2569: \rput(4.5,0.5){signal pump on}
2570: \rput(0.75,0.2){$\ell_3$}
2571: \psframe[framearc=.3](1,0)(2.5,1.5)
2572: \rput(1.7,1.2){$x < 2$}
2573: \rput(1.7,0.8){$\dot{x} = 1$}
2574: \rput(1.7,0.4){$\dot{w} = -2$}
2575: \rput(1.25,2.3){$x = 2$}
2576: \psline{->}(1.75,1.5)(1.75,3)
2577: \rput(2.5,2.3){switch on}
2578:
2579: \endpspicture
2580: }
2581: \end{picture}
2582: }
2583: \caption{Water-level monitor}
2584: \label{fig:water-level-monitor}
2585: \end{figure}
2586: This models a system describing
2587: how the water level in a tank is controlled by a monitor that senses the
2588: water level $w$ and
2589: \ifthenelse{\boolean{TR}}{%%
2590: turns a pump on and off.
2591: }{%%
2592: operates a pump.
2593: }%%\ifthenelse{\boolean{TR}}{%%
2594: When the pump is off, $w$ falls by 2\centimeter per second;
2595: when the pump is on,
2596: $w$ rises by 1\centimeter per second.
2597: However, there is a delay of 2 seconds
2598: from the moment the monitor signals the pump to change
2599: from on to off or vice versa before the switch is actually operated.
2600: Initially the automaton is at $\ell_0$ with
2601: $w = 1$ and it is required that $1 \leq w \leq 12$ at all times.
2602: Thus the monitor must signal the pump to turn on when $w = 5$
2603: and signal it to turn off when $w = 10$.
2604:
2605: The automaton illustrated in \textup{Figure~\ref{fig:water-level-monitor}}
2606: has 2 dimensions with variables $w$ and $x$,
2607: where $x$ denotes the time (in seconds) since the previous,
2608: most recent, signal from the monitor.
2609: There are four locations $\ell_i$ where $i = 0$,~$1$,~$2$,~$3$.
2610: At $\ell_0$ and $\ell_1$ the pump is on,
2611: while at $\ell_2$ and $\ell_3$ the pump is off.
2612: At $\ell_1$ and $\ell_3$ the monitor has signaled
2613: a change to the pump switch, but this has not yet been operated.
2614: Thus we have:
2615: \begin{align*}
2616: &\begin{aligned}
2617: \Init(\ell_0) &= \con\bigl(\{w = 1\}\bigr),
2618: & \Init(\ell_1) &= \Init(\ell_2) = \Init(\ell_3) = \emptyset, \\
2619: \Inv(\ell_0) &= \con\bigl(\{w < 10\}\bigr),
2620: & \Inv(\ell_1) &= \Inv(\ell_3) = \con\bigl(\{x < 2\}\bigr), \\
2621: \Inv(\ell_2) &= \con\bigl(\{w > 5\}\bigr),
2622: & \Act(\ell_0) &= \Act(\ell_1) = \con\bigl(\{\dot{x} = \dot{w} = 1\}\bigr), \\
2623: \end{aligned} \\
2624: & \Act(\ell_2) = \Act(\ell_3) = \con\bigl(\{\dot{x} = 1, \dot{w} = -2\}\bigr).
2625: \end{align*}
2626: There are four transitions
2627: $\tau_{ij} = (\ell_i, a_i, \cP_i, \ell_j) \in \Trans$,
2628: where $i \in \{0,1,2,3\}$ and $j = i+1 \pmod 4$;
2629: the affine relations are
2630: \ifthenelse{\boolean{TR}}{%%
2631: \begin{align*}
2632: \cP_0 &= \con\bigl(\{w = 10, x' = 0, w' = w\}\bigr), \\
2633: \cP_1 &= \con\bigl(\{x = 2, x' = x, w' = w\}\bigr), \\
2634: \cP_2 &= \con\bigl(\{w = 5, x' = 0, w' = w\}\bigr), \\
2635: \cP_3 &= \cP_1.
2636: \end{align*}
2637: }{%%
2638: \begin{align*}
2639: \cP_0 &= \con\bigl(\{w = w' = 10, x' = 0\}\bigr),
2640: &\qquad
2641: \cP_1 &= \con\bigl(\{x = x' = 2, w' = w\}\bigr), \\
2642: \cP_2 &= \con\bigl(\{w = w' = 5, x' = 0\}\bigr),
2643: &\qquad
2644: \cP_3 &= \cP_1.
2645: \end{align*}
2646: }%%\ifthenelse{\boolean{TR}}
2647: \end{example}
2648:
2649: \ifthenelse{\boolean{TR}}{%%
2650: \begin{example}
2651: \label{ex:fischer-protocol}
2652: A graphical representation of an automaton
2653: for a simplified version of the Fischer protocol is given in
2654: \textup{Figure~\ref{fig:fisher-protocol}}.
2655: \begin{figure}
2656: \centering
2657: {\scriptsize
2658: \begin{picture}(330,160)(0,0)
2659: \put(0,0){
2660: \setlength{\unitlength}{0.7pt}%
2661: \psset{xunit=1cm,yunit=1cm,runit=1cm}
2662: \psset{origin={0,0}}
2663: \pspicture*[](-1,-1)(12,10)
2664: \psline{->}(0.5,5.1)(2.95,5.1)
2665: \rput(1.4,5.35){$a \geq 0, b \geq 0,$}
2666: \rput(1.4,4.9){$0 \leq k \leq 2$}
2667: \rput(2.8,5.35){$\ell_0$}
2668: \psframe[framearc=.3](2.95,4.25)(4.85,5.52)
2669: \rput(3.9,5.34){$0 \leq k \leq 2$}
2670: \rput(3.9,5.05){$\dot{x}_1 = 1$}
2671: \rput(3.9,4.75){$9 \leq 10\dot{x}_2 \leq 11$}
2672: \rput(3.9,4.45){$\dot{a} = \dot{b} = 0$}
2673:
2674: \rput(3.9,3.875){$k = 0,\, x_1' = 0$}
2675: \psline{->}(3.875,4.25)(3.875,3.5)
2676:
2677: \rput(2.75,3.3){$\ell_1$}
2678: \psframe[framearc=.3](2.95,2.25)(4.85,3.5)
2679: \rput(3.9,3.34){$x_1 \leq a, k = 0$}
2680: \rput(3.9,3.05){$\dot{x}_1 = 1$}
2681: \rput(3.9,2.75){$9 \leq 10\dot{x}_2 \leq 11$}
2682: \rput(3.9,2.45){$\dot{a} = \dot{b} = 0$}
2683:
2684: \rput(3.5,1.9){$x_1' = x_2' = 0,\, k' = 1$}
2685: \psline{->}(3.875,2.25)(3.875,1.5)
2686: \rput(4.8,2){$$}
2687:
2688: \rput(2.75,1.3){$\ell_2$}
2689: \psframe[framearc=.3](2.95,0.25)(4.85,1.5)
2690: \rput(3.9,1.34){$k = 1$}
2691: \rput(3.9,1.05){$\dot{x}_1 = 1$}
2692: \rput(3.9,0.75){$9 \leq 10\dot{x}_2 \leq 11$}
2693: \rput(3.9,0.45){$\dot{a} = \dot{b} = 0$}
2694:
2695: \psline[linearc=1]{->}(0.875,3.5)(1.05,4.4)(3,4.85)
2696: \rput(0.7,4.3){$x_1 \geq b$}
2697:
2698: \rput(-0.25,3.3){$\ell_3$}
2699: \psframe[framearc=.3](-0.05,2.25)(1.85,3.5)
2700: \rput(0.9,3.34){$k = 2$}
2701: \rput(0.9,3.05){$\dot{x}_1 = 1$}
2702: \rput(0.9,2.75){$9 \leq 10\dot{x}_2 \leq 11$}
2703: \rput(0.9,2.45){$\dot{a} = \dot{b} = 0$}
2704:
2705: \psline[linearc=1]{->}(2.95,0.875)(1.15,1.3)(0.875,2.25)
2706: \rput(0.7,1.5){$x_1 < b, x_2 \leq a,\, k' = 2$}
2707: \rput(1.5,0.8){$$}
2708:
2709: \psline[linearc=1]{->}(4.85,0.875)(5.53,0.875)(6.07,1.32)
2710: \rput(5.8,0.8){$x_1 \geq b$}
2711:
2712: \rput(8.05,2.3){$\ell_4$}
2713: \psframe[framearc=.3](5.95,1.25)(7.85,2.5)
2714: \rput(6.9,2.34){$k = 1$}
2715: \rput(6.9,2.05){$\dot{x}_1 = 1$}
2716: \rput(6.9,1.75){$9 \leq 10\dot{x}_2 \leq 11$}
2717: \rput(6.9,1.45){$\dot{a} = \dot{b} = 0$}
2718:
2719: \rput(6.25,4){$k' = 0$}
2720: \psline[linearc=2]{->}(6.875,2.5)(6,3.8)(4.85,4.5)
2721:
2722: \psline[linearc=1]{->}(7.25,2.5)(7.5,2.6)(7.875,3.25)
2723: \rput(8.5,2.8){$x_2 \leq a, k' = 2$}
2724:
2725: \rput(9.05,4.3){$\ell_5$}
2726: \psframe[framearc=.3](6.95,3.25)(8.85,4.5)
2727: \rput(7.9,4.34){$k = 2$}
2728: \rput(7.9,4.05){$\dot{x}_1 = 1$}
2729: \rput(7.9,3.75){$9 \leq 10\dot{x}_2 \leq 11$}
2730: \rput(7.9,3.45){$\dot{a} = \dot{b} = 0$}
2731:
2732: \rput(6.2,5.15){$\mathit{true}$}
2733: \psline[linearc=2]{->}(6.9,4.2)(6.5,5)(4.85,5.2)
2734:
2735: \endpspicture
2736: }
2737: \end{picture}
2738: }
2739: \caption{Fischer protocol (simplified)}
2740: \label{fig:fisher-protocol}
2741: \end{figure}
2742: This models mutual exclusion for a system with two processors
2743: $P_1$ and $P_2$ with skewed clocks $x_1$ and $x_2$, respectively.
2744: Each processor has a critical
2745: section and, at any one moment in time, at most one may be in its
2746: critical section. This mutual exclusion is ensured by a version of
2747: the Fischer protocol which requires that $P_1$ and $P_2$ share a
2748: variable $k$; a process $P_i$ ($i = 1$,~$2$) is only able to enter its critical
2749: section if $k = i$ and $P_i$ may only write to $k$ if $k=0$. However,
2750: it takes at most $a$ time units, as measured by $P_i$'s clock for
2751: $P_i$ to set the value of $k$ to $i$ and it could be that the other
2752: process $P_j$ may also have started writing $j$ to $k$. To avoid any
2753: resulting conflict, the protocol requires that $P_i$ must wait for a
2754: further $b$ time units, also measured by $P_i$'s clock, before checking
2755: that $k=i$ still holds. The time $b$ is called the \emph{delay time}.
2756: The protocol ensures mutual exclusion only for certain values of $a$
2757: and $b$ which depend on the relative rates of $x_1$ and $x_2$.
2758: Here it is assumed that the rate of
2759: $x_2$ is between 0.9 and 1.1 times that of $x_1$
2760: and that, for $i = 1$,~$2$, the clock $x_i$ is reset to zero
2761: at the start of both the write process and the delay time
2762: for $P_i$.
2763:
2764: The automaton illustrated in \textup{Figure~\ref{fig:fisher-protocol}} has
2765: 5 dimensions with variables $a$, $b$, $x_1$, $x_2$, $k$.
2766: Note that here, $a$ and $b$ are constant for all runs of the automaton
2767: and this is indicated in the graph
2768: by the inclusion of the derivative constraints
2769: $\dot{a} = \dot{b} = 0$ at every location.
2770: There are six locations:
2771: $\ell_0$ where $P_1$ is idle;
2772: at $\ell_1$ where $k=0$ and $P_1$ is in the process of writing to $k$;
2773: at $\ell_2$ where $k=1$ and $P_1$ waits for the delay time of $b$
2774: time units;
2775: at $\ell_3$ where $k=2$ since $P_2$ managed to complete writing
2776: to $k$ before the delay time of $b$ had expired;
2777: at $\ell_4$ where the process $P_1$ is in the critical section;
2778: at $\ell_5$ where $P_2$ has set $k = 2$ and the mutual
2779: exclusion guarantee is violated.
2780: All the functions and transitions for these locations are as given
2781: in \textup{Figure~\ref{fig:fisher-protocol}}.
2782: \end{example}
2783: }{}%% \ifthenelse{\boolean{TR}}
2784:
2785: \begin{example}
2786: \label{ex:scheduler}
2787: A representation of an automaton
2788: for a simple task scheduler is given in \textup{Figure~\ref{fig:scheduler}}.
2789: \begin{figure}[p]
2790: \centering
2791: {\scriptsize
2792: \begin{picture}(330,180)(15,-10)
2793: \put(0,0){
2794: \setlength{\unitlength}{0.7pt}%
2795: \psset{xunit=1cm,yunit=1cm,runit=1cm}
2796: \psset{origin={0,0}}
2797: \pspicture*[](-2.5,-1)(10,10)
2798: \rput(3.6,5.75){\emph{Interrupt}}
2799: \psline{->}(0.5,5.35)(3,5.35)
2800: \rput(1.6,5.6){$c_1 \geq 0, c_2 \geq 0$}
2801: \rput(4.6,5.35){Intpt}
2802: \psframe[framearc=.3](3,4.25)(4.25,5.5)
2803: \rput(3.65,5.3){$\mathit{true}$}
2804: \rput(3.65,4.9){$\dot{c}_1 = 1$}
2805: \rput(3.65,4.5){$\dot{c}_2 = 1$}
2806:
2807: \rput(0.58,4.845){$I_1; c_1 \geq 10, c_1' = 0$}
2808: \pscurve{->}(3,5)(2.3,5.15)(1.75,4.845)(2.3,4.5)(3,4.67)
2809: \pscurve{->}(4.25,5)(4.95,5.15)(5.50,4.845)(4.95,4.5)(4.25,4.67)
2810: \rput(6.7,4.845){$I_2; c_2 \geq 20, c_2' = 0$}
2811:
2812: \rput(3.6,3.75){\emph{Task}}
2813: \psline{->}(0,3.35)(3,3.35)
2814: \rput(1.4,3.6){$x_1 = x_2 = k_1 = k_2 = 0$}
2815: \rput(4.5,3.35){Idle}
2816: \psframe[framearc=.3](3,2.25)(4.25,3.5)
2817: \rput(3.65,3.3){$\mathit{true}$}
2818: \rput(3.65,2.9){$\dot{x}_1 = 0$}
2819: \rput(3.65,2.5){$\dot{x}_2 = 1$}
2820:
2821: \rput(0.4,2.6){$x_1 = 4, k_1 \leq 1,$}
2822: \rput(0.4,2.3){$k_1\minusminus, x_1' = 0$}
2823: \psline[linearc=1]{->}(0.625,1.5)(1.3,2.3)(3,2.825)
2824:
2825: \rput(2.15,1.8){$I_1; k_1' = 1$}
2826: \rput(2.1,1.7){$$}
2827: \psline[linearc=1]{<-}(1.25,1.2)(2.55,1.45)(3.35,2.25)
2828:
2829: \rput(6.8,2.6){$x_2 = 8, k_2 \leq 1, k_1 = 0,$}
2830: \rput(6.8,2.3){$k_2\minusminus, x_2' = 0$}
2831: \psline[linearc=1]{->}(6.625,1.5)(5.8,2.3)(4.25,2.825)
2832:
2833: \rput(5.05,1.8){$I_2; k_2' = 1$}
2834: \rput(5.05,1.7){$$}
2835: \psline[linearc=1]{<-}(6,1.2)(4.7,1.45)(3.9,2.25)
2836:
2837: \rput(1.65,-0.1){Task1}
2838: \psframe[framearc=.3](0,-0.2)(1.25,1.5)
2839: \rput(0.65,1.05){$x_1 \leq 4$}
2840: \rput(0.65,0.65){$\dot{x}_1 = 1$}
2841: \rput(0.65,0.25){$\dot{x}_2 = 0$}
2842:
2843: \rput(5.6,-0.1){Task2}
2844: \psframe[framearc=.3](6,-0.2)(7.25,1.5)
2845: \rput(6.65,1.05){$x_2 \leq 8$}
2846: \rput(6.65,0.65){$\dot{x}_1 = 0$}
2847: \rput(6.65,0.25){$\dot{x}_2 = 1$}
2848:
2849: \rput(3.5,1.1){$I_2; k_2' = 1$}
2850: \psline{->}(1.25,0.9)(6,0.9)
2851: \psline{<-}(1.25,0.6)(6,0.6)
2852: \rput(3.6,0.4){$x_2 = 8, k_2 \leq 1, k_1 \geq 1,$}
2853: \rput(3.6,0.1){$k_2\minusminus, x_2' = 0$}
2854:
2855: \rput(-1.75,1.1135){$I_1; k_1\plusplus$}
2856: \pscurve{->}(0,1.2)(-0.6,1.3)(-1.2,1.075)(-0.6,0.85)(0,0.95)
2857: \rput(-0.6,-0.4){$x_1 = 4, k_1 \geq 2, k_1\minusminus, x_1' = 0$}
2858: \pscurve{->}(0,0.3)(-0.6,0.4)(-1.2,0.175)(-0.6,-0.05)(0,0.05)
2859:
2860: \rput(8.95,1.225){$I_2; k_2\plusplus$}
2861: \pscurve{->}(7.25,1.3)(7.85,1.4)(8.45,1.1865)(7.75,0.975)(7.25,1.075)
2862: \rput(8.95,0.6){$I_1; k_1\plusplus$}
2863: \pscurve{->}(7.25,0.75)(7.85,0.85)(8.45,0.6365)(7.85,0.425)(7.25,0.535)
2864: \rput(8,-0.4){$x_2 = 8, k_2 \geq 1, k_2\minusminus, x_2' = 0$}
2865: \pscurve{->}(7.25,0.2)(7.85,0.3)(8.45,0.0855)(7.85,-0.125)(7.25,-0.025)
2866:
2867: \endpspicture
2868: }
2869: \end{picture}
2870: }
2871: \caption{Scheduler}
2872: \label{fig:scheduler}
2873: \end{figure}
2874: This models a scheduler with two classes of
2875: tasks $A_1$ and $A_2$, activated by interrupts $I_1$ and $I_2$.
2876: Interrupt $I_1$ (resp.,
2877: $I_2$) occurs at most once every 10 (resp., 20) seconds and activates
2878: a task in class $A_1$ (resp., $A_2$), which takes 4 (resp., 8)
2879: seconds to complete.
2880: Tasks in $A_2$ have priority and preempt tasks in $A_1$.
2881: It is required that tasks in $A_2$ never wait.
2882:
2883: The \emph{Scheduler} automaton given in \textup{Figure~\ref{fig:scheduler}}
2884: is the parallel composition of two component automata:
2885: \emph{Interrupt} which models the
2886: assumptions about the interrupt frequencies; and \emph{Task},
2887: which models the execution of the tasks.
2888: The \emph{Interrupt} automaton, which has a single location `Intpt',
2889: has variables
2890: $c_1$ and $c_2$; $c_i$ ($i = 1$,~$2$) measures the
2891: time elapsed since interrupt $I_i$ occurred.
2892: The \emph{Task} automaton has three locations:
2893: `Idle' when no tasks are running;
2894: and `Task1' and `Task2' when tasks in classes $A_1$
2895: (resp., $A_2$) are active.
2896: It has, for each $i = 1$,~$2$, variables
2897: $x_i$, which measures the execution time of task $i$,
2898: and $k_i$, which counts the number of pending tasks in class
2899: task $i$.
2900:
2901: The combined \emph{Scheduler} automaton has variables
2902: $x_1$, $x_2$, $k_1$, $k_2$, $c_1$ and $c_2$ and
2903: locations which are elements of the Cartesian product
2904: of the sets of locations for \emph{Interrupt} and \emph{Task}.
2905: As \emph{Interrupt} has just one location,
2906: each \emph{Task} location $\ell$ is used to denote the
2907: corresponding \emph{Scheduler} location;
2908: here, the initial $\Init(\ell)$, derivative $\Act(\ell)$ and invariant
2909: $\Inv(\ell)$ polyhedra for the \emph{Scheduler}
2910: are the concatenation of the corresponding component polyhedra
2911: for the \emph{Task} and \emph{Interrupt} automata
2912: (informally, a concatenation of polyhedra $\cP \in \Pset_m$ and
2913: $\cQ \in \Pset_n$ can be obtained by first embedding $\cP$ into
2914: a vector space of dimension $n+m$ and then add a suitably renamed-apart
2915: version of the constraints defining~$\cQ$).
2916: %
2917: Each transition $(\ell, a, \cP, \ell')$ in the \emph{Task} automaton
2918: not triggered by interrupts $I_1$ and $I_2$
2919: has a transition $(\ell, a, \cQ, \ell')$ in the product automaton
2920: where $\cQ \in \Pset_6$ is obtained by embedding $\cP$ into
2921: a vector space of dimension $6$.
2922: Letting $i =$~$1$, $2$,
2923: for transitions $(\ell, I_i, \cP, \ell')$
2924: and $(\mathrm{Intpt}, I_i, \cP', \mathrm{Intpt})$
2925: in the \emph{Task} and \emph{Interrupt} automata, respectively,
2926: there is a transition $(\ell, I_i, \cQ, \ell')$
2927: in the product automaton where $\cQ \in \Pset_6$
2928: is obtained by concatenating $\cP$ and $\cP'$.
2929: \end{example}
2930:
2931: Given a linear hybrid automaton, the aim of an analyzer is to check,
2932: or even find sufficient conditions that ensure, that a valid
2933: \emph{run} of the system cannot \emph{reach} a location and vector of
2934: values that violate some requirement of the system. For instance, in
2935: Example~\ref{ex:water-monitor}, we need to show that the water level
2936: always lies between 1\centimeter and 12\centimeter;
2937: \ifthenelse{\boolean{TR}}{%%
2938: in Example~\ref{ex:fischer-protocol}, we need to find conditions on $a$
2939: and $b$ so that at most one processor can be in its critical section at
2940: any one time;
2941: }{}%% \ifthenelse{\boolean{TR}}
2942: in Example~\ref{ex:scheduler}, we need to show
2943: that no task in $A_2$ will ever wait. To show how
2944: polyhedral computations can be used to prove such properties, we first
2945: define more formally such a run and how reachable sets may be computed.
2946: Note that these definitions follow,
2947: with only minor changes, the approach in \cite{HalbwachsPR97}.
2948:
2949: Letting $\cH = (\Loc, \Init, \Act, \Inv, \Lab, \Trans)$
2950: be a linear hybrid automaton in $n$ dimensions,
2951: a \emph{state} $s$ of $\cH$ consists of a pair $(\ell, \vect{v})$,
2952: where $\ell \in \Loc$ and $\vect{v} \in \Inv(\ell)$.
2953: Given states $s = (\ell, \vect{v})$ and $s' = (\ell', \vect{v}')$,
2954: a time delay $t \in \nonnegRset$ and a
2955: vector $\vect{w} \in \Act(\ell)$,
2956: \ifthenelse{\boolean{TR}}{%%
2957: \[
2958: s \timedstep{t}{\vect{w}} s'
2959: \]
2960: }{%%
2961: \(
2962: s \timedstep{t}{\vect{w}} s'
2963: \)
2964: }%% \ifthenelse{\boolean{TR}}
2965: is a \emph{step} of $\cH$ provided that,
2966: for all $t' \in \left[0, t\right)$,
2967: $\vect{v} + t' \vect{w} \in \Inv(\ell)$ and,
2968: for some $(\ell, a, \cP, \ell') \in \Trans$,
2969: \(
2970: (\vect{v} + t \vect{w}) \mathop{::} \vect{v}' \in \cP.
2971: \)
2972: %
2973: A \emph{run} of $\cH$ is a sequence (finite or infinite) of steps
2974: \ifthenelse{\boolean{TR}}{%%
2975: \begin{equation}
2976: \label{eq:automaton-run}
2977: s_0 \timedstep{t_0}{\vect{w}_0} s_1 \timedstep{t_1}{\vect{w}_1} s_2 \cdots
2978: \end{equation}
2979: }{%%
2980: \(
2981: s_0 \timedstep{t_0}{\vect{w}_0} s_1 \timedstep{t_1}{\vect{w}_1} s_2 \cdots
2982: \),
2983: }%%\ifthenelse{\boolean{TR}}{%%
2984: where the initial state $s_0 = (\ell_0, \vect{v}_0)$ satisfies the condition
2985: $\vect{v}_0 \in \Init(\ell_0)$.
2986: %
2987: An infinite run diverges if the sum $\sum_{i\geq 0} t_i$ diverges.
2988: For each divergent run
2989: \ifthenelse{\boolean{TR}}{%%
2990: given by~\eqref{eq:automaton-run}
2991: }{}%%\ifthenelse{\boolean{TR}}
2992: where,
2993: for $i \geq 0$, $s_i = (\ell_i, \vect{v}_i)$,
2994: we associate a (state) \emph{behavior} $\beta$
2995: which is a total function from time to states:
2996: that is, $\beta(0) = s_0$ and, for each $t > 0$,
2997: $\beta(t) \defeq (\ell_i, \vect{v})$, where
2998: \ifthenelse{\boolean{TR}}{%%
2999: \begin{equation*}
3000: i = \min \biggl\{\,
3001: k \in \Nset
3002: \biggm|
3003: \sum_{j=0}^k t_j > t
3004: \,\biggr\}
3005: \qquad \text{and} \qquad
3006: \vect{v} = \vect{v}_i + \vect{w}_i \biggl(t - \sum_{j < i} t_j\biggr).
3007: \end{equation*}
3008: }{%%
3009: \(
3010: i = \min \bigl\{\,
3011: k \in \Nset
3012: \bigm|
3013: \sum_{j=0}^k t_j > t
3014: \,\bigr\}
3015: \)
3016: and
3017: \(
3018: \vect{v} = \vect{v}_i + \vect{w}_i \bigl(t - \sum_{j < i} t_j\bigr)
3019: \).
3020: }%%\ifthenelse{\boolean{TR}}{%%
3021: A state $s$ is \emph{reachable} if there exists a divergent run
3022: with behavior $\beta$ and time $t \in \nonnegRset$ such that
3023: $\beta(t) = s$.
3024: The set of all \emph{reachable values $R_\ell$} for a location $\ell$
3025: is defined as:
3026: \[
3027: R_\ell
3028: \defeq
3029: \bigl\{\,
3030: \vect{v} \in \Rset^n
3031: \bigm|
3032: \exists t \in \nonnegRset \st
3033: \beta(t) = (\ell, \vect{v})
3034: \,\bigr\}.
3035: \]
3036: The set of reachable values $R_\ell$
3037: at a location $\ell$ can be characterized by a system of
3038: fixpoint equations that are defined in terms of
3039: sets of reachable values $R_{\ell'}$ at locations $\ell'$ where
3040: $\bigl(\ell', a, \cP, \ell\bigr) \in \Trans$.
3041: These equations use the following operations on sets of vectors in
3042: $\Rset^n$.
3043: Let $\cP, \cQ \in \Pset_{2n}$ and $S \sseq \Rset^n$. Then
3044: \begin{align*}
3045: \psi_{\cP}(S)
3046: &\defeq
3047: \{\,
3048: \vect{v}' \in \Rset^n
3049: \mid
3050: \vect{v} \in S,
3051: \vect{v} \mathop{::} \vect{v}' \in \cP
3052: \,\};\\
3053: S \timeelapse \cQ
3054: &\defeq
3055: \{\,
3056: \vect{v} + t \vect{w} \in \Rset^n
3057: \mid
3058: \vect{v} \in S, \vect{w} \in \cQ, t \in \nonnegRset
3059: \,\}.
3060: \end{align*}
3061: Note that, if $S \in \Pset_n$, then also $\psi_{\cP}(S) \in \Pset_n$
3062: and $S \timeelapse \cQ \in \Pset_n$.
3063: The `$\mathop{\timeelapse}$' operator,
3064: called the \emph{time elapse} operator, was first proposed
3065: in~\cite{HalbwachsPR97}.
3066: %
3067: We can now provide the fixpoint equation for $R_\ell$:
3068: \begin{equation}
3069: \label{eq:reach-ell}
3070: R_\ell
3071: = \biggl(
3072: \Bigl(
3073: \Init(\ell)
3074: \union
3075: \bigunion_{(\ell', a, \cP, \ell) \in \Trans}
3076: \psi_{\cP}(R_{\ell'}) \inters \Inv(\ell)
3077: \Bigr)
3078: \timeelapse \Act(\ell)
3079: \biggr)
3080: \inters \Inv(\ell).
3081: \end{equation}
3082: Informally, the fixpoint equation for $R_\ell$ says that the
3083: reachable values at the location $\ell$ are obtained by letting the
3084: time elapse either from an initial value for $\ell$ or from a value
3085: obtained from an incoming transition.
3086: However, the fixpoint Equation~\eqref{eq:reach-ell}
3087: cannot handle strict constraints correctly and needs modifying;
3088: this is illustrated in the following example.
3089: %
3090: \begin{example}
3091: \label{ex:water-monitor-reach-all}
3092: Consider again \textup{Example~\ref{ex:water-monitor}}.
3093: Then, just applying \textup{Equation~\eqref{eq:reach-ell}}
3094: \ifthenelse{\boolean{TR}}{%%
3095: (as proposed in~\textup{\cite{HalbwachsPR94,HalbwachsPR97}}),
3096: }{%%
3097: (as proposed in~\textup{\cite{HalbwachsPR97}}),
3098: }%%\ifthenelse{\boolean{TR}}{%%
3099: the sets of reachable values at locations $\ell_1, \ell_2, \ell_3$ are
3100: empty.
3101: The reason for this is that, for example, at location $\ell_0$,
3102: the strict constraint $w < 10$ must hold, while in the transition from
3103: $\ell_0$ to $\ell_1$, the transition condition $w = 10$ has to hold.
3104: On the other hand, it follows from the definition of a step,
3105: that since one of the derivative constraints at $\ell_0$ is
3106: $\dot{w} = 1$; the water level $w$ may continue to increase
3107: up to the topological closure of $R_{\ell_0}$
3108: which is consistent with $w = 10$.
3109: \end{example}
3110: %
3111: To resolve this problem,
3112: in Equation~\eqref{eq:reach-ell} defining the concrete computation,
3113: $R_{\ell'}$ needs to be replaced by
3114: \ifthenelse{\boolean{TR}}{%%
3115: \begin{equation}
3116: \label{eq:reach-ell-strict}
3117: c(R_{\ell'})
3118: \inters
3119: \bigl(R_{\ell'} \timeelapse \Act(\ell')\bigr),
3120: \end{equation}
3121: }{%%
3122: \(
3123: c(R_{\ell'})
3124: \inters
3125: \bigl(R_{\ell'} \timeelapse \Act(\ell')\bigr)
3126: \),
3127: }%%\ifthenelse{\boolean{TR}}{%%
3128: where $c(R_\ell')$ denotes the topological closure of $R_\ell' \sseq \Rset^n$.
3129:
3130: \ifthenelse{\boolean{TR}}{%%
3131: Observe that, although the linear hybrid automata
3132: are specified by means of polyhedra,
3133: the reachable set $R_\ell$ for a linear hybrid automaton and location $\ell$
3134: may not be in the form of a convex polyhedron.
3135: Thus, to verify that some states of an automaton are unreachable
3136: using the standard polyhedral computations,
3137: approximations are needed.
3138: In particular,
3139: in the fixpoint Equation~\eqref{eq:reach-ell}
3140: (or \eqref{eq:reach-ell-strict}),
3141: the set operations have to be replaced
3142: by the corresponding polyhedral operations.
3143: In fact all the operations in \eqref{eq:reach-ell} except set union
3144: can be used as they are, since they transform polyhedra to polyhedra.
3145: Just the set union operation has to be replaced by the poly-hull operation
3146: `$\polyhull$' described in Section~\ref{sec:preliminaries}.
3147: }{%%\ifthenelse{\boolean{TR}}{%%
3148: Observe that, although the linear hybrid automata
3149: are specified by means of polyhedra,
3150: the reachable set $R_\ell$ for a linear hybrid automaton and location $\ell$
3151: may not be a convex polyhedron since Equation~\eqref{eq:reach-ell}
3152: uses the set union operation.
3153: Therefore, to verify that some states of an automaton are unreachable
3154: using standard polyhedral computations,
3155: set union has to be replaced by the poly-hull operation
3156: $\polyhull$ described in Section~\ref{sec:preliminaries}.
3157: }%%\ifthenelse{\boolean{TR}}{%%
3158: Thus the following fixpoint equation computes an approximation
3159: $R_\ell^\sharp$ to the reachability set~$R_\ell$.
3160: \begin{equation}
3161: \label{eq:reach-ell-sharp}
3162: R_\ell^\sharp =
3163: \biggl(
3164: \Bigl(
3165: \Init(\ell) \polyhull
3166: \biguplus_{(\ell', a, \cP, \ell) \in \Trans}
3167: \psi_{\cP}(R_{\ell'}^\sharp) \inters \Inv(\ell)
3168: \Bigr)
3169: \timeelapse \Act(\ell)
3170: \biggr)
3171: \inters \Inv(\ell).
3172: \end{equation}
3173: As for the concrete fixpoint equation,
3174: to correctly handle the strict constraints
3175: \ifthenelse{\boolean{TR}}{%%
3176: Equation~\eqref{eq:reach-ell-sharp}
3177: needs to be modified by replacing $R_{\ell'}^\sharp$ with
3178: \[
3179: c(R_{\ell'}^\sharp)
3180: \inters
3181: \bigl(R_{\ell'}^\sharp \timeelapse \Act(\ell')\bigr).
3182: \]
3183: }{%%
3184: in Equation~\eqref{eq:reach-ell-sharp}
3185: we need to replace $R_{\ell'}^\sharp$ with
3186: \(
3187: c(R_{\ell'}^\sharp)
3188: \inters
3189: \bigl(R_{\ell'}^\sharp \timeelapse \Act(\ell')\bigr)
3190: \).
3191: }%%\ifthenelse{\boolean{TR}}{%%
3192:
3193: \ifthenelse{\boolean{TR}}{%%
3194: If we let $\vect{R}^\sharp$ denote the tuple
3195: $\{\, R_\ell^\sharp \mid \ell \in \Loc \,\}$
3196: we can write Equation~\eqref{eq:reach-ell-sharp} as
3197: \[
3198: R_\ell^\sharp = F_\ell(\vect{R}^\sharp).
3199: \]
3200: For all $\ell \in \Loc$, we write
3201: $\vect{R}_\ell^{\sharp(0)} = \emptyset$ and, for all $k \geq 1$,
3202: $\vect{R}_\ell^{\sharp(k+1)} = F_\ell(\vect{R}_\ell^{\sharp(k)})$.
3203: Then $\vect{R}^\sharp$ can be computed iteratively provided the sequence
3204: $\vect{R}^{\sharp(0)}, \vect{R}^{\sharp(1)}, \ldots$ does not diverge.
3205: To handle diverging sequences, we apply a widening
3206: (see Section~\ref{sec:widening}).
3207: Note that we do not have to apply it at all locations.
3208: Let $\cW$ be a set of locations that cut all cyclic paths
3209: in the graph of the hybrid automaton (that is, each loop
3210: of the directed graph contains at least one location in $\cW$).
3211: Then the following set of fixpoint equations is guaranteed to converge:
3212: \begin{equation}
3213: \label{eq:reach-ell-sharp-with-widening}
3214: R_\ell^\sharp
3215: =
3216: \begin{cases}
3217: R_\ell^\sharp \widen F_\ell(\vect{R}^\sharp),
3218: &\text{ if $\ell \in \cW$;} \\
3219: F_\ell(\vect{R}^\sharp),
3220: &\text{ if $\ell \in \Loc \setdiff \cW$.}
3221: \end{cases}
3222: \end{equation}
3223: }{%%
3224: If we let $\vect{R}^\sharp$ denote the tuple
3225: $\{\, R_\ell^\sharp \mid \ell \in \Loc \,\}$
3226: we can write Equation~\eqref{eq:reach-ell-sharp} as
3227: \(
3228: R_\ell^\sharp = F_\ell(\vect{R}^\sharp)
3229: \).
3230: For all $\ell \in \Loc$, we write
3231: $\vect{R}_\ell^{\sharp(0)} = \emptyset$ and, for all $k \geq 1$,
3232: $\vect{R}_\ell^{\sharp(k+1)} = F_\ell(\vect{R}_\ell^{\sharp(k)})$.
3233: Then $\vect{R}^\sharp$ can be computed iteratively provided the sequence
3234: $\vect{R}^{\sharp(0)}, \vect{R}^{\sharp(1)}, \ldots$ does not diverge.
3235: To handle diverging sequences, we apply a widening
3236: (see Section~\ref{sec:widening});
3237: note that this only needs to be applied at sufficient locations
3238: so that each cyclic path
3239: in the graph of the hybrid automaton has at least one widening point.
3240: }%%\ifthenelse{\boolean{TR}}{%%
3241:
3242: \begin{example}
3243: \label{ex:water-monitor-abstract}
3244: Consider again \textup{Example~\ref{ex:water-monitor}}.
3245: As there is a single loop passing through $\ell_0$,
3246: it is sufficient to define the set of widening locations
3247: as
3248: \ifthenelse{\boolean{TR}}{%%
3249: $\cW = \{\ell_0\}$.
3250: }%%\ifthenelse{\boolean{TR}}{%%
3251: {%%
3252: $\{\ell_0\}$.
3253: }%%\ifthenelse{\boolean{TR}}{%%
3254:
3255: With the modified form of \textup{Equation~\eqref{eq:reach-ell-sharp}} and
3256: the polyhedra widening of~\textup{\cite{CousotH78}},
3257: the computation requires three
3258: iterations resulting in polyhedra defined by constraint systems
3259: $\cC_i$ for $0 \leq i \leq 3$ where:
3260: \begin{align*}
3261: \cC_0 &= \{ 1 \leq w < 10 \},
3262: & \quad
3263: \cC_1 &= \{ w - x = 10,\, 10 \leq w < 12 \}, \\
3264: \cC_2 &= \{ w + 2x = 16,\, 5 < w \leq 12 \},
3265: & \quad
3266: \cC_3 &= \{ w + 2x = 5,\, 1 < w \leq 5 \}.
3267: \end{align*}
3268: \end{example}
3269: \ifthenelse{\boolean{TR}}{%%
3270: \begin{example}
3271: \label{ex:fischer-protocol-abstract}
3272: Consider again \textup{Example~\ref{ex:fischer-protocol}}.
3273: The analysis terminates without widening in
3274: just two iterations with the resulting polyhedron at~$\ell_5$
3275: defined by the constraint system:
3276: \begin{multline*}
3277: \cC = \{
3278: k = 2,\,
3279: 10a \geq 9b,\,
3280: 0 \leq b \leq x_1,\,
3281: 9x_1 \leq 10x_2 \leq 11x_1, \\
3282: 11x_1 + 10a \geq 10x_2 + 11b
3283: \}.
3284: \end{multline*}
3285: It therefore follows that, to ensure that there can be no run
3286: with a state at location $\ell_5$, it is sufficient that $10a < 9b$.
3287: \end{example}
3288: }{}%% \ifthenelse{\boolean{TR}}
3289:
3290: \begin{example}
3291: \label{ex:scheduler-abstract}
3292: Consider again \textup{Example~\ref{ex:scheduler}}.
3293: By applying the above mentioned polyhedra widening
3294: at location `Task2' only,
3295: the analysis for the product automaton terminates in four iterations.
3296: \ifthenelse{\boolean{TR}}{%
3297: After projecting away the variables $c_1$ and $c_2$,
3298: the reachable values are given by polyhedra
3299: defined by constraint systems $\cC_{t0}$, $\cC_{t1}$, and $\cC_{t2}$
3300: for locations `Idle', `Task1' and `Task2', respectively, where:
3301: \begin{align*}
3302: \cC_{t0} &=
3303: \{ x_1 = x_2 = k_1 = k_2 = 0 \},\\
3304: \cC_{t1} &=
3305: \{ 0 \leq x_1 \leq 4,\, x_2 = 0,\, k_1 = 1,\, k_2 = 0 \},\\
3306: \cC_{t2} &=
3307: \{ x_2 \geq 0,\, x_2 \leq 8,\, 4k_1 \geq x_1,\, x_1 \geq 0,\, k_2 = 1 \}.
3308: \end{align*}
3309: So it can be concluded that, at each location of the automaton, $k_2 \leq 1$
3310: and, hence, no task in class $A_2$ will ever have to wait.
3311: }{%%
3312: After projecting onto variables $k_1$ and $k_2$,
3313: the reachable values are given by polyhedra
3314: defined by constraint systems $\cC_{t0}$, $\cC_{t1}$, and $\cC_{t2}$
3315: for locations `Idle', `Task1' and `Task2', respectively, where:
3316: \begin{equation*}
3317: \cC_{t0}
3318: = \{ k_1 = k_2 = 0 \},
3319: \quad
3320: \cC_{t1} = \{ k_2 = 0,\, k_1 = 1 \},
3321: \quad
3322: \cC_{t2}
3323: = \{ k_2 = 1 \}.
3324: \end{equation*}
3325: Therefore, since at all locations $k_2 \leq 1$,
3326: no task in class $A_2$ will ever have to wait.
3327: }%\ifthenelse{\boolean{TR}}{%
3328: However, as noted in~\textup{\cite{HalbwachsPR97}},
3329: because of the convex hull approximation,
3330: with the polyhedral domain the
3331: analyzer fails to show that $k_1 \leq 2$.
3332: \ifthenelse{\boolean{TR}}{%
3333: We therefore redid the analysis using a domain of powersets of
3334: polyhedra (see \textup{Section~\ref{sec:generalizations-of-polyhedra}})
3335: and, after taking the poly-hull of the final
3336: sets and projecting away the variables $c_1$ and $c_2$,
3337: we obtained the polyhedra
3338: defined by constraint systems $\cC'_{t0}$, $\cC'_{t1}$ and $\cC'_{t2}$
3339: for locations `Idle', `Task1' and `Task2', respectively, where:
3340: \begin{align*}
3341: \cC'_{t0}
3342: &= \{ x_1 = x_2 = k_1 = k_2 = 0 \}, \\
3343: \cC'_{t1}
3344: &= \{ 0 \leq x_1 \leq 4,\, x_2 = 0,\, k_1 = 1,\, k_2 = 0 \}, \\
3345: \cC'_{t2}
3346: &= \{ 0 \leq x_1 \leq 4,\, 0 \leq x_2 \leq 8,\,
3347: 4k_1 \geq x_1 \geq 2k_1 - 2, \\
3348: & \qquad \qquad \qquad \qquad \qquad
3349: x_1 + x_2 \geq 10k_1 - 10,\,
3350: k_1 \leq 2,\, k_2 = 1 \}.
3351: \end{align*}
3352: This verifies that $k_1 \leq 2$ and $k_0 \leq 1$
3353: in every state of any run of the automata.
3354: }{%%
3355: We therefore redid the analysis using a domain of powersets of
3356: polyhedra (see \textup{Section~\ref{sec:generalizations-of-polyhedra}})
3357: and, after taking the poly-hull of the final
3358: sets and projecting onto variables $k_1$ and $k_2$,
3359: we obtained the polyhedra
3360: defined by constraint systems $\cC'_{t0}$, $\cC'_{t1}$ and $\cC'_{t2}$
3361: for locations `Idle', `Task1' and `Task2', respectively, where:
3362: \begin{equation*}
3363: \cC'_{t0}
3364: = \{ k_1 = k_2 = 0 \},
3365: \quad
3366: \cC'_{t1}
3367: = \{ k_2 = 0,\, k_1 = 1 \},
3368: \quad
3369: \cC'_{t2}
3370: = \{ k_1 \leq 2,\, k_2 = 1 \}.
3371: \end{equation*}
3372: }%%\ifthenelse{\boolean{TR}}
3373: \end{example}
3374:
3375: Hybrid systems with affine or nonlinear dynamics do not fit the above
3376: specification of a linear system so that the verification techniques
3377: described here are not directly applicable. Nonetheless, by
3378: partitioning the continuous state space and over-approximating the
3379: dynamics in each of the partitions, the same techniques used to verify
3380: linear hybrid automata can be used in these more general cases
3381: \ifthenelse{\boolean{TR}}{%%
3382: \cite{DoyenHR05,Frehse05,HenzingerH95b,HenzingerHW97b,SankaranarayananSM06}.
3383: }{%%
3384: \cite{DoyenHR05,Frehse05,HenzingerHW97b}.
3385: }%\ifthenelse{\boolean{TR}}
3386: Such an approach has also been successfully applied in the
3387: verification of analog circuits, as discussed in the following
3388: section.
3389:
3390: \section{Analysis and Verification of Analog Systems}
3391: \label{sec:analysis-of-analog-systems}
3392:
3393: The idea of applying formal methods, that originated in the digital
3394: world, to analog systems was put forward in \cite{HartongHB02}.
3395: This is an important step forward with
3396: respect to more traditional methods for the validation of analog
3397: circuit designs. A formal verification tool can, for example, ensure
3398: that a design satisfies certain properties for entire sets of initial
3399: states and continuous ranges of circuit parameters, something that
3400: cannot be done with simulation.
3401:
3402: \ifthenelse{\boolean{TR}}{%%
3403: In \cite{DangDM04} and \cite{GuptaKR04}, polyhedral approximations
3404: were successfully used in the verification of analog circuits.
3405: Here, we use a simple example, taken from \cite{FrehseKR06},
3406: on the verification of an oscillator circuit to
3407: illustrate the approach.%
3408: \footnote{For a more general view, we refer the interested reader
3409: to the cited literature and to \cite{Maler06}.}
3410: }{%%
3411: To illustrate the approach, we describe a simple example of
3412: verification of an oscillator circuit, taken from \cite{FrehseKR06}.
3413: }%%\ifthenelse{\boolean{TR}}{%%
3414: To verify properties of the (cyclic) behavior of such circuits, cyclic
3415: invariants have to be determined. To establish a cyclic invariant for
3416: a given set of initial states and ranges for the circuit parameters,
3417: one has to show that the circuit returns to a subset of those initial
3418: states, which implies the system will keep traversing the same states
3419: indefinitely.
3420: \ifthenelse{\boolean{TR}}{%%
3421: From such an invariant, a number of properties of the
3422: oscillator can be established \cite{FrehseKRM06}.
3423: }{}%%\ifthenelse{\boolean{TR}}{%%
3424:
3425: \ifthenelse{\boolean{TR}}{}{%%
3426: \begin{figure}
3427: \begin{minipage}[b]{0.4\linewidth}
3428: \centering
3429: \subfigure[Circuit schematic]%
3430: {\label{fig:tunnel-diode-oscillator-schematic}%
3431: \parbox[t]{\linewidth}%
3432: {\centering
3433: \setlength{\unitlength}{0.240900pt}
3434: \begin{picture}(300,360)(-20,20)
3435: \put(-300,0){
3436: \psset{xunit=0.7cm,yunit=0.7cm,runit=0.7cm}
3437: \psset{origin={0,0}}
3438: \pspicture*[](10,4)
3439: \psset{dipolestyle=elektor}
3440: \pnode(2,3){Vin}
3441: \pnode(1.5,3){S} \pnode(3.5,3){A} \pnode(6.5,3){B} \pnode(7.7,3){C}
3442: \pnode(1.5,1){Sm}\pnode(3.5,1){Am}\pnode(6.5,1){Bm}\pnode(7.7,1){Cm}
3443: \Ucc[dipoleconvention=generator,tension,tensionoffset=0.8,labeloffset=1.2](Sm)(S){$V_\mathrm{in}$}
3444: \resistor[dipolestyle=rectangle](Vin)(A){$R$}
3445: \coil[dipolestyle=elektorcurved,intensitylabel=$I_L$](A)(B){$L$}
3446: \diode[dipoleconvention=receptor,intensitylabel=$I_d$,tensionlabel=$V_d$,tensionoffset=-0.5,tensionlabeloffset=-0.9,](B)(Bm){}
3447: \capacitor(C)(Cm){$C$}
3448: \psset{intensitylabel=}
3449: \wire(Am)(Bm)
3450: \wire(Bm)(Cm)
3451: \wire(B)(C)
3452: \wire(S)(Vin)
3453: \wire(Sm)(Am)
3454: \pscircle*(B){2\pslinewidth}
3455: \pscircle*(Bm){2\pslinewidth}
3456: \endpspicture
3457: }
3458: \end{picture}
3459: }} \\
3460: \subfigure[Tunnel diode characteristic]%
3461: {\label{fig:tunnel-diode-characteristic}%
3462: \parbox[t]{\linewidth}%
3463: {\centering
3464: \input diode.tex
3465: }}
3466: \end{minipage}
3467: \begin{minipage}[b]{0.6\linewidth}
3468: \centering
3469: \subfigure[Reachable states (dashed)]%
3470: {\label{fig:tunnel-diode-oscillator-invariant}%
3471: \parbox[b]{\linewidth}%
3472: {\centering
3473: \rotatebox{90}{$\qquad\qquad\qquad I_L [\milliampere]$}%
3474: \includegraphics*[scale=0.45, bb = 105 205 488 576]{tdo_results.eps} \\
3475: $\quad\quad V_d [\volt]$
3476: }
3477: \rotatebox{90}{\quad\footnotesize{(Picture courtesy of Goran Frehse.)}}
3478: }
3479: \end{minipage}
3480: \caption{Tunnel-diode oscillator circuit}
3481: \label{fig:tunnel-diode-oscillator}
3482: \end{figure}
3483: }%%\ifthenelse{\boolean{TR}}
3484:
3485: Consider the tunnel-diode oscillator schematized
3486: in Figure~\ref{fig:tunnel-diode-oscillator-schematic}.
3487: \ifthenelse{\boolean{TR}}{%%
3488: \begin{figure}
3489: \subfigure[Circuit schematic]%
3490: {\label{fig:tunnel-diode-oscillator-schematic}%
3491: \parbox{0.5\linewidth}%
3492: {\centering
3493: \setlength{\unitlength}{0.240900pt}
3494: \begin{picture}(300,360)(-20,20)
3495: \put(-300,0){
3496: \psset{xunit=0.7cm,yunit=0.7cm,runit=0.7cm}
3497: \psset{origin={0,0}}
3498: \pspicture*[](10,4)
3499: \psset{dipolestyle=elektor}
3500: \pnode(2,3){Vin}
3501: \pnode(1.5,3){S} \pnode(3.5,3){A} \pnode(6.5,3){B} \pnode(8.5,3){C}
3502: \pnode(1.5,1){Sm}\pnode(3.5,1){Am}\pnode(6.5,1){Bm}\pnode(8.5,1){Cm}
3503: \Ucc[dipoleconvention=generator,tension,tensionoffset=0.8,labeloffset=1.2](Sm)(S){$V_\mathrm{in}$}
3504: \resistor[dipolestyle=rectangle](Vin)(A){$R$}
3505: \coil[dipolestyle=elektorcurved,intensitylabel=$I_L$](A)(B){$L$}
3506: \diode[dipoleconvention=receptor,intensitylabel=$I_d$,tensionlabel=$V_d$,tensionoffset=-0.5,tensionlabeloffset=-0.9,](B)(Bm){}
3507: \capacitor(C)(Cm){$C$}
3508: \psset{intensitylabel=}
3509: \wire(Am)(Bm)
3510: \wire(Bm)(Cm)
3511: \wire(B)(C)
3512: \wire(S)(Vin)
3513: \wire(Sm)(Am)
3514: \pscircle*(B){2\pslinewidth}
3515: \pscircle*(Bm){2\pslinewidth}
3516: \endpspicture
3517: }
3518: \end{picture}
3519: }}%
3520: \subfigure[Tunnel diode characteristic]%
3521: {\label{fig:tunnel-diode-characteristic}%
3522: \parbox{0.5\linewidth}%
3523: {\centering
3524: \input diode.tex
3525: }}
3526: \caption{Tunnel-diode oscillator circuit}
3527: \label{fig:tunnel-diode-oscillator}
3528: \end{figure}
3529: }{}%%\ifthenelse{\boolean{TR}}{%%
3530: The state of the system at a given instant of time is completely characterized
3531: by the values of the inductor current $I_L$ and the diode voltage drop $V_d$.
3532: With these as the state variables, the system is described by the
3533: second-order state equations
3534: \ifthenelse{\boolean{TR}}{%%
3535: \begin{align}
3536: \label{eq:tdo-Vd/dt}
3537: \dot{V}_d &= 1/C\bigl(-I_d(V_d) + I_L\bigr), \\
3538: \label{eq:tdo-IL/dt}
3539: \dot{I}_L &= 1/L(-V_d -R I_L + V_\mathrm{in}).
3540: \end{align}
3541: }{%%
3542: $\dot{V}_d = 1/C\bigl(-I_d(V_d) + I_L\bigr)$
3543: and
3544: $\dot{I}_L = 1/L(-V_d -R I_L + V_\mathrm{in})$.
3545: }%%\ifthenelse{\boolean{TR}}{%%
3546: In \cite{FrehseKR06} it is shown how a cyclic invariant can be obtained
3547: for this circuit using the PHAVer system. First, a piecewise affine envelope
3548: is constructed for the tunnel diode characteristic $I_d(V_d)$ depicted
3549: in Figure~\ref{fig:tunnel-diode-characteristic}: for the particular
3550: example analyzed in \cite{FrehseKR06}, sufficient precision is obtained
3551: by dividing the range $V_d \in [-0.1\volt, 0.6\volt]$
3552: \ifthenelse{\boolean{TR}}{%%
3553: into $64$ intervals,
3554: resulting in a piecewise affine model of~\eqref{eq:tdo-Vd/dt}.
3555: }{%%
3556: into $64$ intervals.
3557: }%%\ifthenelse{\boolean{TR}}{%%
3558: Forward reachability computation with PHAVer can obtain the
3559: set of states depicted in Figure~\ref{fig:tunnel-diode-oscillator-invariant}.
3560: \ifthenelse{\boolean{TR}}{%%
3561: \begin{figure}
3562: \hfill
3563: \parbox[t]{0.5\linewidth}%
3564: {\centering
3565: \rotatebox{90}{$\qquad\qquad\qquad\qquad I_L [\milliampere]$}%
3566: \includegraphics*[scale=0.5, bb = 105 205 488 576]{tdo_results.eps} \\
3567: $\qquad\qquad V_d [\volt]$
3568: }
3569: \hfill
3570: \rotatebox{90}{\qquad\quad\footnotesize{(Picture courtesy of Goran Frehse.)}}
3571: \caption{Reachable states of the tunnel-diode oscillator (dashed)}
3572: \label{fig:tunnel-diode-oscillator-invariant}
3573: \end{figure}
3574: }{}%%\ifthenelse{\boolean{TR}}{%%
3575: These are the states reachable from the set of initial states corresponding
3576: to $V_d \in [0.42\volt, 0.52\volt]$ and $I_L = 0.6 \milliampere$
3577: (the base of the downward-facing triangular shape in
3578: Figure~\ref{fig:tunnel-diode-oscillator-invariant}).
3579: \ifthenelse{\boolean{TR}}{%%
3580: Taking into account that
3581: }{%%
3582: As
3583: }%%\ifthenelse{\boolean{TR}}{%%
3584: the loop shape constituted by the reachable states
3585: is traversed clockwise, it can be seen that the inductor current $I_L$ returns
3586: to the initial value of $0.6 \milliampere$ with a diode voltage drop
3587: that is well within the initial range $[0.42\volt, 0.52\volt]$.
3588: The set of reachable states so obtained is thus an invariant of
3589: the circuit.
3590:
3591: In \cite{FrehseKR06} it is shown that, due to over-approximation, forward
3592: reachability can fail to determine invariants of more complex circuits.
3593: A new technique combining forward and backward reachability with iterative
3594: refinement of the partitions is thus proposed and shown to be more powerful
3595: and efficient.
3596:
3597: \ifthenelse{\boolean{TR}}{%%
3598: \section{Families of Polyhedral Approximations for Analysis and Verification}
3599: }{%%
3600: \section{Families of Polyhedral Approximations}
3601: }%%\ifthenelse{\boolean{TR}}{%%
3602: \label{sec:families-of-polyhedral-approximations}
3603:
3604: For several applications of static analysis and verification,
3605: an approximation based on the domain of convex polyhedra can be
3606: regarded as the most appropriate choice.
3607: In this section we discuss alternative options (simplifications,
3608: generalizations, and combinations with other numerical domains)
3609: that might be considered when trying either to reduce the cost
3610: of the analysis, or to increase the precision of the computed results.
3611:
3612: \subsection{Simplifications of Polyhedra}
3613: \label{sec:simplifications-of-polyhedra}
3614:
3615: \ifthenelse{\boolean{TR}}{%%
3616: There are contexts where approximations based on the domain of
3617: }{%%
3618: There are contexts where approximations based on general
3619: }%% \ifthenelse{\boolean{TR}}
3620: convex polyhedra, no matter which implementation is adopted,
3621: incur an unacceptable computational cost.
3622: In such cases, the static analysis may resort to further simplifications
3623: so as to obtain useful results within reasonable time and space bounds.
3624:
3625: A first, almost traditional approach is based on the identification
3626: of suitable syntactic subclasses of polyhedra.
3627: %%
3628: The abstract domain of \emph{bounding boxes} (or intervals~\cite{CousotC76})
3629: is based on polyhedra that can be represented as finite conjunctions
3630: of constraints of the form $\pm x_i \leq d$ or $\pm x_i < d$,
3631: leading to the specification of operations whose worst-case complexity
3632: is linear in the number of space dimensions.
3633: %%
3634: As a more precise alternative, the class of \emph{potential constraints}
3635: \ifthenelse{\boolean{TR}}{%%
3636: \cite{AllenK85,Bagnara97th,Bellman57,Davis87,Dill89,LarsenLPY97},
3637: also known as \emph{bounded differences},
3638: }{%%
3639: \cite{Bellman57},
3640: also known as \emph{bounded differences} \cite{Bagnara97th,Davis87},
3641: }%% \ifthenelse{\boolean{TR}}
3642: allows for constraints
3643: of the form $x_i - x_j \leq d$ or $\pm x_i \leq d$;
3644: \ifthenelse{\boolean{TR}}{%%
3645: the generalization proposed in~\cite{BalasundaramK89},
3646: also admits constraints of the form $x_i + x_j \leq d$,
3647: leading to the abstract domain of \emph{octagons}~\cite{Mine01b}.
3648: }{%%
3649: the abstract domain of \emph{octagons}~\cite{Mine05th}
3650: also admits constraints of the form $x_i + x_j \leq d$.
3651: }%%\ifthenelse{\boolean{TR}}{%%
3652: In these last two cases, the operators are characterized by a worst-case
3653: time complexity which is cubic in the number of space dimensions.
3654: %%
3655: For all of the approximations mentioned above, improved efficiency also
3656: follows from the fact that the corresponding computations are simple enough
3657: to allow for the adoption of floating-point data types: in contrast,
3658: the specification of safe and efficient floating-point operations
3659: for general polyhedra is an open problem, so that polyhedra libraries
3660: have to be based on unbounded precision data types.
3661:
3662: Several alternative (syntactic and/or semantic) simplification schemes
3663: have been put forward in the recent literature.
3664: %%
3665: The \emph{Two Variables per Linear Inequality} abstract domain
3666: is proposed in~\cite{SimonKH02},
3667: where constraints take the syntactic form $ax_i + bx_j \leq d$.
3668: %%
3669: In~\cite{SankaranarayananSM05}, an arbitrary family of polyhedra
3670: is chosen before starting the analysis by fixing the slopes of a
3671: finite number of linear inequalities,
3672: which are called the \emph{template constraints};
3673: linear programming techniques are then used to compute precise
3674: approximations in the considered class of shapes.
3675: %%
3676: In contrast, in~\cite{SankaranarayananCSM06}, general polyhedra are allowed,
3677: but the corresponding operations (in particular, the poly-hull and the image
3678: of affine relations) are approximated by less precise variants so as
3679: to ensure a polynomial worst-case complexity in the size of the inputs.
3680: %%
3681: An even more flexible approach is proposed in~\cite{Frehse05},
3682: where arbitrary polyhedra are approximated, when they become too complex,
3683: by limiting the number of constraints in their description and/or
3684: the magnitude of the coefficients occurring in the constraints.
3685: %%
3686: These more dynamic approximation schemes are promising,
3687: in particular for those applications where nothing is known in advance
3688: about the syntactic form of the constraints that will be computed
3689: during the analysis.
3690:
3691: An important observation to be made is that there is no actual need
3692: to prefer \emph{a priori} (and therefore commit to) a specific
3693: abstract domain: the analysis tool may be based on several abstractions,
3694: safely switching from more precise, possibly costly domains to more
3695: efficient, possibly imprecise ones, and vice versa, depending on the context.
3696: %%
3697: When replacing a generic polyhedron by a simpler one,
3698: the problem of the identification of a good over-approximation
3699: has to be solved.
3700: Depending on the context, the approaches may vary significantly.
3701: At one extreme, when efficiency is really critical, the adoption
3702: of syntactic techniques should be pursued:
3703: for an interesting example, we refer the reader to one of the
3704: simplification heuristics used in~\cite{Frehse05}, where the efficient
3705: selection of a small number of linear inequalities out of
3706: a constraint system is driven by a simple, yet effective reasoning
3707: on the measure of the angles formed by the corresponding half-spaces.
3708: At the other extreme, linear programming (LP) optimization techniques
3709: may be used so as to obtain the best match in the considered
3710: class of geometric shapes. For instance, the precise approximation
3711: of a polyhedron by a bounding box (resp., a bounded difference
3712: or octagon) can be implemented by a linear (resp., quadratic) number
3713: of optimizations of a class of LP problems, where the objective function
3714: varies while the feasible region is invariant and defined by the
3715: constraints of the polyhedron.
3716: Note that, if correctness has to be preserved, it is essential that no
3717: rounding error is made on the wrong side, so that classical
3718: floating-point implementations of LP solvers have to be considered unsafe,
3719: unless the computed results can be certified by some other tool.
3720: Alternatively, it is possible to consider LP implementations based on
3721: unbounded precision data types.
3722:
3723: When the number of space dimensions to be modeled is beyond a given
3724: threshold, the whole analysis space can be split into a finite number
3725: of smaller, more manageable components, thereby realizing a further
3726: simplification scheme that can be combined with those described above.
3727: The splitting strategy varies considerably.
3728: %%
3729: \ifthenelse{\boolean{TR}}{%%
3730: In~\cite{HalbwachsMG06,HalbwachsMP-V03}, Cartesian factoring techniques
3731: }{%%
3732: In~\cite{HalbwachsMG06}, Cartesian factoring techniques
3733: }%%\ifthenelse{\boolean{TR}}{%%
3734: are used so as to dynamically partition the space dimensions of
3735: a polyhedron into independent subsets; the orthogonal factors are then
3736: approximated by lower dimensional polyhedra with no precision penalty.
3737: %%
3738: In an alternative approach described in~\cite{BlanchetCCFMMMR03}, many
3739: (possibly overlapping) small subsets of space dimensions, called
3740: \emph{variable packs}, are identified before the start of the
3741: analysis by means of syntactic conditions; the relations holding
3742: between the variables in each pack are then approximated by using an
3743: octagonal abstraction.
3744: %%
3745: A variation of this is described in~\cite{VenetB04},
3746: where non-overlapping variable packs are dynamically computed
3747: (and possibly merged) during the analysis, whereas the relations
3748: between the variables in a pack are approximated by means of
3749: potential constraints. In~\cite{VenetB04} it is also observed that,
3750: since the average size of variables packs is small (5 variables),
3751: more precise approximations based on general polyhedra should be feasible.
3752:
3753: \subsection{Generalizations of Polyhedra}
3754: \label{sec:generalizations-of-polyhedra}
3755:
3756: There are applications where the restriction to the domain of convex
3757: polyhedra is intrinsically inadequate. This may happen, not only when
3758: the verification property of interest is itself non-convex,
3759: but also when the adopted computation strategy requires that a
3760: convex property is proved by passing through a non-convex
3761: intermediate approximation.
3762: This was the case in Example~\ref{ex:scheduler-abstract} of
3763: Section~\ref{sec:analysis-of-hybrid-systems}, where the upper bound
3764: ($k_1 \leq 2$) on the number of waiting processes for class $A_1$
3765: was obtained by switching from the domain of convex polyhedra
3766: to the domain of finite sets of polyhedra.
3767:
3768: \ifthenelse{\boolean{TR}}{%%
3769: The finite powerset domain construction~\cite{Bagnara98SCP}
3770: }{%%
3771: The finite powerset domain construction~\cite{Bagnara98SCP}
3772: }%%\ifthenelse{\boolean{TR}}{%%
3773: is a special case of \emph{disjunctive completion}~\cite{CousotC79},
3774: a systematic technique to derive an enhanced abstract domain
3775: starting from an existing one. A finite powerset domain
3776: implements disjunctions by maintaining an explicit (hence finite)
3777: and \emph{non-redundant} collection of elements of the base-level domain:
3778: non-redundancy means that a collection is made of maximal elements
3779: with respect to the approximation ordering, so that no element
3780: subsumes another element in the collection.
3781:
3782: For a better understanding of the concepts, which are described
3783: in completely general terms in~\cite{BagnaraHZ06STTT},
3784: let us consider the application of the finite powerset construction
3785: to the domain of convex polyhedra.
3786: This instantiation (which is the one also adopted for the examples
3787: developed in~\cite{BagnaraHZ06STTT}) can be used to model nonlinear
3788: systems as described, e.g., in Section~\ref{sec:analysis-of-analog-systems}.
3789: Then, an element of the abstract domain is a finite set of maximal
3790: convex polyhedra, so that no polyhedron in the set is contained in
3791: another polyhedron in the set.
3792: The powerset domain is a lattice: the bottom and top elements
3793: are $\emptyset$ and $\{ \Rset^n \}$, respectively;
3794: the meet is obtained by removing redundancies from the set of all possible
3795: binary intersections of an element in the first powerset with an element
3796: in the second powerset; while the binary join is the non-redundant subset of
3797: the union of the two arguments.
3798: %%
3799: Most of the other abstract operations needed for a static analysis
3800: using the finite powerset domain are easily obtained by ``lifting''
3801: the corresponding operations defined on the base-level domain,
3802: and then reinforcing non-redundancy. For instance, the computation
3803: of the image of a finite powerset under an affine relation is obtained
3804: by computing the image of each polyhedron in the collection.
3805: However, the construction of a provably correct widening operator
3806: has only recently been addressed in~\cite{BagnaraHZ06STTT}
3807: (see Section~\ref{sec:widening}).
3808: %%
3809: The generic specification of the abstract operators of
3810: the finite powerset domain in terms of abstract operations
3811: on the (arbitrary) base-level domain allows for the development
3812: of a single implementation which is shared by all the possible
3813: instances of the domain construction.
3814:
3815: An alternative abstraction scheme has been proposed in~\cite{BagnaraR-CZ05}
3816: for the case of finite conjunctions of polynomial inequalities.
3817: Intuitively, a polynomial constraint can be approximated by means of
3818: a linear constraint in a higher dimension vector space, so that the
3819: different terms of the polynomial (e.g., $x_0$, $x_0x_1$, $x_0^2$) are mapped
3820: to different and independent space dimensions; these linear constraints
3821: are then used to perform an almost classical linear relation analysis
3822: based on convex polyhedra.
3823: Due to the linearization step, most of the precision of the polynomial
3824: constraints is initially lost; however, some of the relations holding
3825: between the different terms of the original polynomial can be recovered
3826: by adding further constraints that are redundant when interpreted
3827: in the polynomial world, but do contribute to precision in the
3828: linearized space. In particular, in~\cite{BagnaraR-CZ05}
3829: the polynomial constraints are mapped into finitely generated
3830: \emph{polynomial cones} and a degree-bounded product closure operator
3831: is systematically applied so as to improve accuracy.
3832: %%
3833: As a trivial example, let the polynomial terms $x_0$, $x_1$ and $x_0x_1$
3834: be mapped to the space dimensions $y_0$, $y_1$ and $y_2$, respectively.
3835: Then, the linearization of the polynomial constraints $x_0 \geq 0$
3836: and $x_1 \geq 0$ will produce a polyhedron that,
3837: while satisfying $y_0 \geq 0$ and $y_1 \geq 0$,
3838: leaves variable $y_2$ totally unconstrained.
3839: By applying the product closure operator we also obtain
3840: the linear constraint $y_2 \geq 0$,
3841: thereby recovering the non-negativity of term $x_0x_1$.
3842:
3843:
3844: \subsection{Combinations with other Numerical Abstractions}
3845: \label{sec:other-abstractions}
3846:
3847: \ifthenelse{\boolean{TR}}{%%
3848: We observe that there
3849: }{%%
3850: There
3851: }%%\ifthenelse{\boolean{TR}}{%%
3852: are two basic kinds of numerical abstractions for
3853: approximating the values of the program variables:
3854: outer \emph{limits} (or bounds within which the values must lie)
3855: and the pattern of \emph{distribution} of these values.
3856: The first can be approximated by (constructions based on)
3857: convex polyhedra, while the second can be approximated
3858: by sets of congruences defining lattices of points
3859: \ifthenelse{\boolean{TR}}{%%
3860: we call \emph{grids}~\cite{BagnaraDHMZ07,Granger91,Granger97}.
3861: }{%%
3862: we call \emph{grids}~\cite{BagnaraDHMZ07,Granger97}.
3863: }%%\ifthenelse{\boolean{TR}}{%%
3864: Before considering how these and similar domains may be combined,
3865: we give a brief overview of the domain of grids.
3866:
3867: Any vector that satisfies
3868: $\langle \vect{a}, \vect{v} \rangle = b + \mu f$,
3869: for some $\mu \in \Zset$, is said to \emph{satisfy} the
3870: congruence relation $\langle \vect{a}, \vect{v} \rangle \equiv_f b$.
3871: A \emph{congruence system} $\cK$ is a finite set of congruence
3872: relations in $\Rset^n$. A \emph{grid} is the set of all vectors in
3873: $\Rset^n$ that satisfy the congruences in $\cK$. The domain of grids
3874: $\Gset_{n}$ is the set of all grids in $\Rset^n$ ordered by
3875: the set inclusion relation, so that the empty set and $\Rset^n$ are the
3876: bottom and top elements of $\Gset_n$ respectively and the intersection
3877: of two grids is itself a grid. Thus, as for the domain of
3878: polyhedra, the domain of grids forms a lattice
3879: $(\Gset_n, \sseq, \emptyset, \Rset^n, \polyhull, \inters)$
3880: where $\polyhull$ denotes the join
3881: operation returning the least grid greater than or equal to the two
3882: arguments. For more details concerning all aspects of the domain of grids,
3883: see~\cite{BagnaraDHMZ07}.
3884:
3885: The distribution information captured by grids has a number
3886: of applications in its own right: for instance, to ensure that
3887: external memory accesses obey the alignment restriction imposed by the
3888: host architecture, and to enable several transformations for efficient
3889: parallel execution as well as optimizations that enhance cache
3890: behavior. However, here we are primarily concerned with applications
3891: that can benefit from the combination of the domain of grids with that of
3892: convex polyhedra. For instance, knowing the frequency (and position)
3893: of the points in a grid, we can shrink the polyhedra so that the
3894: bounding hyperplanes pass through the grid values; if this leads to a
3895: polyhedron with reduced dimension (such as a single point) or one that
3896: is empty, it can lead, not only to improved precision, but also a more
3897: efficient use of resources by
3898: the analyzer~\cite{Ancourt91th,NookalaR00,QuintonRR96}.
3899:
3900: Generic constructions, such as direct and reduced product, can be used
3901: to provide a formal basis for the combination of the grid and
3902: polyhedral domains \cite{CousotC79} although the exact choice of
3903: product construction used to build the grid-polyhedral domain needs
3904: further study. Both the direct and reduced products have problems:
3905: the direct product has no provision for communication between the
3906: component domains, thereby losing precision; while the reduced
3907: product, which is the most precise refinement of the direct product,
3908: has exponential complexity. It is expected that, for grid-polyhedra,
3909: the most useful product construction will lie between these
3910: extremes. For instance, as equalities are common entities for both
3911: constraint and congruence systems, if an equality is found to hold in
3912: one component, it is safe to just add this to the other component. In
3913: addition, in an element of the grid-polyhedral domain, any hyperplane
3914: that bounds the polyhedron component could be moved inwards until it
3915: intersects with points of the grid with only linear cost on the number
3916: of dimensions. Of course, this reduction on its own is not optimal
3917: since the grid points in the intersection may not lie in the
3918: polyhedron itself. For optimality or, more generally, so as to gain
3919: additional precision, we need to experiment with various forms of the
3920: branch-and-bound and cutting-plane algorithms~\cite{KrishnanM06}
3921: already well-researched for integer linear programming. What is
3922: needed is a range of options for the product construction allowing the
3923: user to decide on the complexity/precision trade-off. Further work on
3924: this is needed, including an investigation of other proposals for generic
3925: products that lie between the direct and reduced product, such as the
3926: local decreasing iteration method~\cite{Granger92} and the open
3927: product construction~\cite{CortesiLCVH00}.
3928:
3929: \section{Polyhedral Computations Peculiar to Analysis and Verification}
3930: \label{sec:peculiar-polyhedral-computations}
3931:
3932: As observed in the previous sections, the analysis of the run-time
3933: behavior of a system can be broken down into a set of
3934: basic operations on the chosen abstract domains.
3935: This means that each abstract domain should provide adequate computational
3936: support for such a set and, where
3937: appropriate, further operations that might be useful for tuning the
3938: cost/precision ratio. In this section, we discuss several key issues
3939: relevant to the design and implementation of an abstract domain of,
3940: or based on, convex polyhedra.
3941: Before going into further detail, it should be stressed that the
3942: particular context of the application plays a significant and
3943: non-trivial role here.
3944: For instance, in many computational complexity studies,
3945: it is assumed that a small number of operations (often, just a single one)
3946: can have arbitrarily large operands;
3947: also, it is typically required that exact results have to be computed.
3948: These assumptions taken together may be inappropriate in the
3949: context of static analysis:
3950: it is quite often the case that a large number of operations will
3951: have only small or medium sized operands; also, whenever
3952: facing an efficiency issue, the exactness requirement can be dropped
3953: (provided soundness is maintained).
3954: As a consequence, the evaluation of alternative algorithmic strategies
3955: should be largely based on practical experimentation.
3956:
3957: \subsection{The Double Description Method}
3958: \label{sec:double-description}
3959:
3960: Convex polyhedra are typically specified by a finite system
3961: of linear inequality constraints and for this representation
3962: there are known algorithms
3963: (e.g., based on Fourier-Motzkin elimination~\cite{LassezM92,Schrijver99})
3964: for most of the operations already mentioned.
3965:
3966: An alternative approach is based on the \emph{double description} method
3967: due to Motzkin et al.~\cite{MotzkinRTT53}. This method was originally defined
3968: on the set of topologically closed convex polyhedra, a sub-lattice
3969: \(
3970: (\CPset_n, \sseq, \emptyset, \Rset^n, \polyhull, \union)
3971: \)
3972: of the lattice of (not necessarily closed, or NNC) polyhedra $\Pset_n$.
3973: In the double description method, a closed polyhedron may be described by
3974: using a system of non-strict linear inequalities or by using
3975: a \emph{generator} system that records its key geometric features.
3976: The following is the main theoretical result,
3977: which is a simple consequence of well-known theorems
3978: by Minkowski and Weyl~\cite{StoerW70}.
3979:
3980: \begin{theorem}
3981: \label{thm:minkowski-weyl}
3982: The set $\cP \sseq \Rset^n$ is a topologically closed convex polyhedron
3983: if and only if there exist finite sets $R, P \sseq \Rset^n$
3984: of cardinality $r$ and $p$, respectively,
3985: such that $\vect{0} \notin R$ and
3986: $\cP$ can be generated from $(R, P)$ as follows:
3987: \[
3988: \cP = \{\,
3989: R \vect{\rho} + P \vect{\pi} \in \Rset^n
3990: \mid
3991: \vect{\rho} \in \nonnegRset^r,
3992: \vect{\pi} \in \nonnegRset^p,
3993: \textstyle{\sum_{i=1}^p \pi_i = 1}
3994: \,\}.
3995: \]
3996: \end{theorem}
3997:
3998: \noindent
3999: Intuitively, a point of a polyhedron $\cP$ is obtained by adding
4000: a convex combination of the vectors in $P$ (the generating points)
4001: to a conic combination of the vectors in $R$ (the generating \emph{rays}).
4002: %%The polyhedron is empty if and only if $P$ is empty.
4003:
4004: It turns out that constraint and generator descriptions are duals:
4005: each representation can be computed starting from the other one.
4006: Clever implementations of this conversion procedure, improving on the
4007: \ifthenelse{\boolean{TR}}{%%
4008: Chernikova's algorithms~\cite{Chernikova64,Chernikova65,Chernikova68},
4009: }{%%
4010: Chernikova's algorithm~\cite{Chernikova68},
4011: }%%\ifthenelse{\boolean{TR}}{%%
4012: are the starting point for the development of software libraries that,
4013: while being characterized by a worst case computational cost which is
4014: exponential in the size of the input, turn out to be practically useful.
4015: A common characteristic of these implementations is the exploitation
4016: of \emph{incrementality}, whereby most of the computational work
4017: done for an operation is reused to efficiently compute small variations
4018: of the corresponding result.
4019: Further computational enhancements are obtained by the adoption of
4020: suitable heuristics, ranging from the efficient handling
4021: of adjacency information~\cite{LeVerge92}, to a careful choice of
4022: ordering strategies for the computation of intermediate
4023: results~\cite{Avis00,AvisB95,FukudaP96};
4024: the overall construction typically relies on a tight integration
4025: of the basic algorithms with a carefully chosen set of data structures
4026: \ifthenelse{\boolean{TR}}{%%
4027: \cite{PPL-USER-0-9}.
4028: }{%%
4029: \cite{BagnaraHZ08SCP}.
4030: }%%\ifthenelse{\boolean{TR}}{%%
4031:
4032: An important motivation for the adoption of an implementation
4033: based on the double description method is that the ability to switch
4034: from a constraint description to a generator description, or vice versa,
4035: can be usefully exploited to provide simple implementations for the
4036: basic operations on polyhedra.
4037: For instance, set intersection is easily implemented by taking the union
4038: of the constraint systems representing the two arguments,
4039: whereas the poly-hull is implemented by joining the generator systems
4040: representing the two arguments;
4041: and the test for emptiness can be implemented by checking that
4042: the generator system has no points.
4043: Moreover, a test for subset inclusion $\cP \sseq \cQ$ can be
4044: implemented by checking if each point and each ray in a generator
4045: system describing $\cP$ satisfies all linear inequalities in a
4046: constraint system describing $\cQ$.
4047: %%
4048: As a further example, the time elapse operation specified
4049: in Section~\ref{sec:analysis-of-hybrid-systems},
4050: can be implemented using the generator systems for the argument
4051: polyhedra~\cite{HalbwachsPR97}.
4052: That is a generator system for the polyhedron $\cP \timeelapse \cQ$
4053: can be obtained by adopting the same set of generating points as $\cP$ and
4054: by defining its set of rays as the union of
4055: the set of generating rays for $\cP$ with the set of
4056: all the generators (both points and rays) for $\cQ$.
4057:
4058: As seen in Section~\ref{sec:analysis-of-computer-programs},
4059: in the context of the analysis of imperative languages
4060: one of the most frequent statements is variable assignment,
4061: where the expression assigned is safely approximated by
4062: an affine relation $\reld{\psi}{\Rset^n}{\Rset^n}$.
4063: The (direct or inverse) image of an affine relation can be naively
4064: computed by embedding the input polyhedron $\cP \sseq \Rset^n$ into
4065: the space $\Rset^{2n}$, intersecting it with the constraints
4066: defining $\psi$ and finally projecting the result back on $\Rset^n$.
4067: However, due to the moves to/from a higher dimensional space,
4068: this approach suffers from significant overheads.
4069: Quite often, the expression assigned is a simple affine function of
4070: the variables' values and can thus be exactly modeled by computing
4071: the image of a single-update affine function.
4072: %% : it is therefore important
4073: %% that such a frequent special case is implemented as efficiently as possible.
4074: With the double description method, the images of affine functions
4075: are much more efficiently computed by applying them
4076: directly to the generators of the argument
4077: polyhedron.
4078: A dual approach, using the constraint description of the polyhedron,
4079: allows for the computation of the preimages of affine functions,
4080: which can be of interest for a backward semantic construction,
4081: where the initial values of program variables are approximated
4082: starting from their final values.
4083: Similar efficiency arguments motivate the study of specific implementations
4084: for single-update bounded affine relations and other special subclasses
4085: of affine relations.
4086:
4087:
4088: \subsection{Widening and Narrowing}
4089: \label{sec:widening}
4090:
4091: The first widening operator for the domain of convex polyhedra,
4092: the so-called \emph{standard widening}
4093: \ifthenelse{\boolean{TR}}{%%
4094: proposed in \cite{CousotH78} and refined in \cite{Halbwachs79th},
4095: }{%%
4096: proposed in \cite{CousotH78},
4097: }%% \ifthenelse{\boolean{TR}}{%%
4098: can be informally described as follows:
4099: suppose that in the post-fixpoint iteration sequence we compute
4100: as successive iterates the polyhedra $\cP_i$ and $\cP_{i+1}$;
4101: then, the widening keeps all and only the constraints defining $\cP_i$
4102: that are also satisfied by $\cP_{i+1}$.
4103: This simple idea, which is basically borrowed from the widening operator
4104: defined on the domain of intervals~\cite{CousotC76}, is quite effective
4105: in ensuring the termination of the analysis (the number of constraints
4106: decreases at each iteration);
4107: by avoiding the application of the widening in the first few
4108: \ifthenelse{\boolean{TR}}{%%
4109: iterations of the analysis~\cite{Cousot81}
4110: }{%%
4111: iterations of the analysis
4112: }%%\ifthenelse{\boolean{TR}}{%%
4113: and/or by applying the ``widening up-to'' technique of~\cite{Halbwachs93},
4114: it also provides, in the main, an adequate level of precision.
4115:
4116: Some application fields, however, are particularly sensitive to
4117: the precision of the deduced numerical information, to the point
4118: that some authors propose to give up the termination guarantee
4119: and use so-called \emph{extrapolation} operators: examples include
4120: the operators defined in \cite{HenzingerH95} and \cite{HenzingerPW01},
4121: %%for the \textsc{HyTech} system,
4122: as well as the proposals in \cite{BultanGP99} and \cite{DelzannoP99}
4123: for sets of polyhedra and
4124: the heuristics sketched in \cite{BessonJT99}.
4125:
4126: In~\cite{BagnaraHRZ05SCP} this precision problem is
4127: reconsidered in a more general context and a framework is proposed
4128: that is able to improve upon the precision of a given widening
4129: while keeping the termination guarantee. The approach, which
4130: builds on theoretical results put forward in work on
4131: termination analysis, combines an existing widening
4132: operator, whose termination guarantee should be \emph{formally certifiable},
4133: with an arbitrary number of precision improving heuristics.
4134: Its feasibility was demonstrated by instantiating the framework
4135: so as to produce a new widening on polyhedra improving upon the
4136: \ifthenelse{\boolean{TR}}{%%
4137: precision of~\cite{Halbwachs79th}
4138: }{%%
4139: precision of the standard widening
4140: }%% \ifthenelse{\boolean{TR}}{%%
4141: in a significant percentage of benchmarks.
4142:
4143: For the more challenging case of an abstract domain obtained
4144: by the finite powerset domain construction, several generic
4145: schemes of widenings have been proposed in~\cite{BagnaraHZ06STTT}
4146: that are able to ``lift'' a widening defined on the base-level domain
4147: without compromising its termination guarantee.
4148: The instantiation of such a generic approach led to the definition
4149: of the first non-trivial and provably correct widenings
4150: on a domain of finite sets of convex polyhedra.
4151: %%
4152: Being highly parametric, the widening schemes proposed
4153: in~\cite{BagnaraHZ06STTT} can be instantiated according to
4154: the needs of the specific application, as done in~\cite{GulavaniR06}.
4155: %%
4156: One of the heuristic approaches adopted in~\cite{BagnaraHZ06STTT}
4157: to control the precision/complexity trade-off of the widenings,
4158: originally proposed in~\cite{BultanGP99}, attempts at reducing
4159: the cardinality of a polyhedral collection by merging
4160: two of its elements whenever their set union happens to be a convex
4161: polyhedron. The implementation of such a heuristic could significantly
4162: benefit from the results and algorithms presented
4163: \ifthenelse{\boolean{TR}}{%%
4164: in~\cite{BaranyF05,BemporadFT01}.
4165: }{%%
4166: in~\cite{BemporadFT01}.
4167: }%%\ifthenelse{\boolean{TR}}{%%
4168:
4169: It is also worth mentioning that, once a post-fixpoint approximation
4170: has been obtained by means of an upward iteration sequence with widening,
4171: its precision can be improved by means of a downward iteration,
4172: possibly using a \emph{narrowing operator}
4173: \ifthenelse{\boolean{TR}}{%%
4174: \cite{CousotC76,CousotC77,CousotC92fr,CousotC92plilp}.
4175: }{%%
4176: \cite{CousotC76,CousotC92fr}.
4177: }%%\ifthenelse{\boolean{TR}}{%%
4178: To the best of our knowledge, no narrowing has ever been defined on
4179: the domain of convex polyhedra: applications simply stop the downward
4180: computation after a small number of iterations.
4181:
4182: \subsection{Not Necessarily Closed Convex Polyhedra}
4183: \label{sec:nnc-polyhedra}
4184:
4185: Most static analysis applications computing linear
4186: inequality relations between program variables
4187: consider the domain $\CPset_n$ of topologically closed polyhedra.
4188: One of the underlying motivations is that sometimes (e.g., when
4189: working with integer valued variables only) strict inequalities
4190: can be filtered away by suitable syntactic manipulations;
4191: even when this is not the case, the topological closure approximation
4192: may be interpreted as a quick and practical workaround to the fact that
4193: some software libraries do not fully support computations on
4194: NNC polyhedra. However, there are applications
4195: \ifthenelse{\boolean{TR}}{%%
4196: \cite{AlurCHH93,ColonS01,HalbwachsPR94,HalbwachsPR97}
4197: }{%%
4198: \cite{AlurCHH93,ColonS01,HalbwachsPR97}
4199: }%%\ifthenelse{\boolean{TR}}{%%
4200: where the ability of encoding and propagating strict inequalities
4201: might be crucial for the usefulness
4202: of the final results.
4203:
4204: The first proposal for a systematic implementation of strict
4205: inequalities in a software library based on the double description method
4206: \ifthenelse{\boolean{TR}}{%%
4207: was put forward in~\cite{HalbwachsPR94}:
4208: }{%%
4209: was put forward in~\cite{HalbwachsPR97}:
4210: }%%\ifthenelse{\boolean{TR}}{%%
4211: a syntactic translation embeds
4212: an $n$-dimensional NNC polyhedron $\cP \in \Pset_n$
4213: into an $(n+1)$-dimensional closed polyhedron $\cR \in \CPset_{n+1}$,
4214: by adding a single \emph{slack variable} $\epsilon$, satisfying
4215: the additional side constraints $0 \leq \epsilon \leq 1$.
4216: Namely, any strict inequality constraint
4217: $\langle \vect{a}, \vect{x} \rangle > b$
4218: is translated into the non-strict inequality constraint
4219: $\langle \vect{a}, \vect{x} \rangle - \epsilon \geq b$.
4220: The computation is thus performed on the closed representation
4221: $\cR \in \CPset_{n+1}$, with only minor adaptations to the basic
4222: algorithms so as to
4223: \ifthenelse{\boolean{TR}}{%%
4224: also
4225: }{}%%\ifthenelse{\boolean{TR}}{%%
4226: take into account the \emph{implicit}
4227: strict constraint $\epsilon > 0$.
4228:
4229: While this idea is quite effective, the resulting software library
4230: no longer enjoys all of the properties of the underlying double
4231: description implementation: NNC polyhedra cannot be suitably described
4232: using generator systems, and the geometric intuitions are
4233: lost under the ``implementation details.''
4234: These problems motivated the studies
4235: \ifthenelse{\boolean{TR}}{%%
4236: in~\cite{BagnaraHZ03a,BagnaraHZ05FAC,BagnaraRZH02},
4237: }{%%
4238: in~\cite{BagnaraHZ05FAC},
4239: }%%\ifthenelse{\boolean{TR}}{%%
4240: where a proper generalization of the double description method
4241: to NNC polyhedra was proposed.
4242: The main improvement was the identification of the \emph{closure point}
4243: as a new kind of generator for NNC polyhedra, leading to the following
4244: result generalizing Theorem~\ref{thm:minkowski-weyl}:
4245:
4246: \begin{theorem}
4247: \label{thm:NNC-minkowski-weyl}
4248: The set $\cP \sseq \Rset^n$ is an NNC polyhedron if and only if
4249: there exist finite sets $R, P, C \sseq \Rset^n$
4250: of cardinality $r$, $p$ and $c$
4251: %%, respectively,
4252: such that $\vect{0} \notin R$ and
4253: \ifthenelse{\boolean{TR}}{%%
4254: \[
4255: \cP
4256: = \sset{
4257: R \vect{\rho} + P \vect{\pi} + C \vect{\gamma} \in \Rset^n
4258: }{
4259: \vect{\rho} \in \nonnegRset^r,
4260: \vect{\pi} \in \nonnegRset^p, \vect{\pi} \neq \vect{0},
4261: \vect{\gamma} \in \nonnegRset^c, \\
4262: \sum_{i=1}^p \pi_i + \sum_{i=1}^c \gamma_i = 1
4263: }.
4264: \]
4265: }{%%
4266: \[
4267: \cP
4268: = \bigl\{\,
4269: R \vect{\rho} + P \vect{\pi} + C \vect{\gamma}
4270: \bigm|
4271: \vect{\rho} \in \nonnegRset^r,
4272: \vect{\pi} \in \nonnegRset^p \setminus \{ \vect{0} \},
4273: \vect{\gamma} \in \nonnegRset^c,
4274: \textstyle{\sum_{i=1}^p} \pi_i
4275: + \textstyle{\sum_{i=1}^c} \gamma_i = 1
4276: \,\bigr\}.
4277: \]
4278: }%\ifthenelse{\boolean{TR}}{%%
4279: \end{theorem}
4280:
4281: \noindent
4282: The new condition $\vect{\pi} \neq \vect{0}$ ensures that
4283: at least one of the points of $P$ plays an active role
4284: in any convex combination of the vectors of $P$ and $C$.
4285: As a consequence, the vectors of $C$ are closure points of $\cP$,
4286: i.e., points that belong to the topological closure of $\cP$,
4287: but may not belong to $\cP$ itself.
4288:
4289: Thanks to the introduction of (strict inequalities and) closure
4290: points, most of the pros of the double description method now also
4291: \ifthenelse{\boolean{TR}}{%%
4292: apply to the domain of NNC polyhedra:
4293: }{%%
4294: apply to the domain of NNC polyhedra~\cite{BagnaraHZ05FAC}:
4295: }%%\ifthenelse{\boolean{TR}}{%%
4296: simpler, higher-level
4297: implementations of operations on NNC polyhedra can be specified,
4298: reasoned about and justified in terms of any one of the two dual
4299: descriptions; important implementation issues (such as the need to
4300: identify and remove all kinds of redundancies in the
4301: \ifthenelse{\boolean{TR}}{%%
4302: descriptions~\cite{BagnaraHZ05FAC,BagnaraRZH02})
4303: }{%%
4304: descriptions)
4305: }%%\ifthenelse{\boolean{TR}}{%%
4306: can be provided with proper
4307: solutions; different lower-level encodings
4308: (e.g., an alternative management of the
4309: \ifthenelse{\boolean{TR}}{%%
4310: slack variable~\cite{BagnaraHZ03a,BagnaraHZ05FAC})
4311: }{%%
4312: slack variable)
4313: }%%\ifthenelse{\boolean{TR}}{%%
4314: can be investigated and experimented with, without affecting the user
4315: of the software library.
4316: It would be interesting, from both a theoretical and practical
4317: point of view, to provide a more direct encoding of NNC polyhedra, i.e.,
4318: one that is not based on the use of slack variables; this requires
4319: the specification and the corresponding proof of correctness of a
4320: direct NNC conversion algorithm, potentially achieving a major
4321: efficiency improvement.
4322:
4323: \section{Conclusion}
4324: \label{sec:conclusion}
4325:
4326: In the field of automatic analysis and verification of software and
4327: hardware systems,
4328: approximate reasoning on numerical quantities is crucial.
4329: As first recognized in 1978 \cite{CousotH78},
4330: polyhedral computation algorithms can be used for the automatic
4331: inference of numerical assertions that correctly (though usually
4332: not completely) characterize the behavior of a system at some
4333: level of abstraction.
4334:
4335: Until the end of the 1990's these techniques were not in
4336: widespread use, mainly due to the unavailability of robust and
4337: efficient implementations of convex polyhedra.
4338: As far as we know, the first published libraries of polyhedral algorithms
4339: suitable for analysis and verification purposes have been
4340: \emph{Polylib},%
4341: \TRfootnote{\url{http://www.ee.byu.edu/faculty/wilde/polyhedra.html}.}
4342: released in 1995, written by Wilde at IRISA \cite{Wilde93th}
4343: and based on earlier work by Le~Verge \cite{LeVerge92},
4344: and the polyhedra library of \emph{POLINE} (POLyhedra INtegrated Environment)
4345: written by Halbwachs and Proy at Verimag and also released in 1995.
4346: Both libraries used machine integers to represent the coefficients of
4347: linear equalities and inequalities, something that could easily result
4348: into (undetected) overflows. While Polylib provided only a fraction of the
4349: functionalities offered by POLINE's library (which offered, among other
4350: things, support for NNC polyhedra), it was available in source
4351: format. The POLINE's library, instead, was distributed only in binary
4352: form for the Sun-4 platform (freely, until about the year 1996; under rather
4353: restrictive conditions afterward). POLINE included also a system called
4354: POLKA (POLyhedra desK cAlculator) and an analyzer for linear hybrid automata.
4355: A variation of a subset of POLINE's library was incorporated into the
4356: \emph{HyTech} tool~\cite{HenzingerHW97b}.%
4357: \TRfootnote{\url{http://embedded.eecs.berkeley.edu/research/hytech/}.}
4358:
4359: The work of Wilde and Le~Verge,
4360: which was extended by Loechner \cite{Loechner99},
4361: led to the creation of \emph{PolyLib}.%
4362: \TRfootnote{\url{http://icps.u-strasbg.fr/polylib/}.}
4363: The \emph{New Polka} library by Jeannet,%
4364: \TRfootnote{\url{http://pop-art.inrialpes.fr/people/bjeannet/newpolka/index.html}.}
4365: first released in 2000 and originally based on both IRISA's Polylib
4366: and POLINE's library, incorporates the idea
4367: ---suggested by Fukuda and Prodon \cite{FukudaP96}---
4368: of lexicographically sorting the matrices representing constraints and
4369: generators.
4370: New Polka, which supports both closed and NNC polyhedra,
4371: together with Min\'e's \emph{Octagon Abstract Domain Library}
4372: \ifthenelse{\boolean{TR}}{%%
4373: \cite{Mine01b,Mine05th}%
4374: }{%%
4375: \cite{Mine05th}%
4376: }%%\ifthenelse{\boolean{TR}}{%%
4377: \TRfootnote{\url{http://www.di.ens.fr/~mine/oct/}}
4378: and an interval library called \emph{ITV}, is now included in
4379: the \emph{APRON} library.%
4380: \TRfootnote{\url{http://apron.cri.ensmp.fr/library/}.}
4381: Finally, the \emph{Parma Polyhedra Library} (PPL),
4382: initially inspired by New Polka and first released in 2001,
4383: is developed and maintained by the authors of this paper.%
4384: \TRfootnote{\url{http://www.cs.unipr.it/ppl}.}
4385: The PPL supports both closed and NNC polyhedra, bounding boxes,
4386: bounded difference and octagonal shapes, grids and combinations
4387: of the above including the finite powerset construction
4388: \ifthenelse{\boolean{TR}}{%%
4389: \cite{BagnaraHZ06TR,BagnaraHZ08SCP}.
4390: }{%%
4391: \cite{BagnaraHZ08SCP}.
4392: }%%\ifthenelse{\boolean{TR}}{%%
4393:
4394:
4395: The above libraries have all been designed specifically for
4396: applications of analysis and verification such as those described
4397: in this paper. However, two libraries that were designed for solving vertex
4398: enumeration/convex hull problems have successfully been used in
4399: static analysis and computer-aided verification tools:
4400: Fukuda's \emph{cddlib},%
4401: \TRfootnote{\url{http://www.ifor.math.ethz.ch/~fukuda/cdd_home/}.}
4402: an implementation of the double description method \cite{MotzkinRTT53};
4403: and \emph{lrslib},%
4404: \TRfootnote{\url{http://cgm.cs.mcgill.ca/~avis/C/lrs.html}.}
4405: the implementation by Avis of the reverse search algorithm \cite{Avis00}.
4406:
4407: All the libraries mentioned in the last two paragraphs are distributed under
4408: free software licenses and support the use of unbounded numeric coefficients.
4409: This, together with the ever increasing available computing power and
4410: the growing interest in ensuring the correctness of critical systems,
4411: has caused, in the 2000's, the continuous emergence of new tools and
4412: applications of polyhedral computations in the area of formal methods.
4413: As a consequence, this is much more of a new beginning than an end
4414: to research in this area.
4415: As explained in
4416: Sections~\ref{sec:families-of-polyhedral-approximations}
4417: and~\ref{sec:peculiar-polyhedral-computations}, several open issues remain.
4418: Most of them have to do with the need for effectively managing the
4419: complexity-precision trade-off: the encouraging results obtained with
4420: today's tools are pushing us to apply them to more complex systems
4421: for a possibly
4422: more precise analysis and/or verification of more complex properties.
4423:
4424: \ifthenelse{\boolean{TR}}{%%
4425: \section*{Acknowledgments}
4426: We thank Goran Frehse for the discussion we had on the subject of polyhedra
4427: simplifications and for contributing the PostScript code we used to produce
4428: Figure~\ref{fig:tunnel-diode-oscillator-invariant}.
4429: }{%%
4430: \textbf{Acknowledgments\ }
4431: We thank Goran Frehse for the discussion we had on polyhedra
4432: simplifications and for the PostScript code for
4433: Figure~\ref{fig:tunnel-diode-oscillator-invariant}.
4434: }%%\ifthenelse{\boolean{TR}}{%%
4435:
4436: %\bibliographystyle{elsart-num-sort}
4437: %\bibliography{ppl,ppl_citations,mybib}
4438:
4439: \ifthenelse{\boolean{TR}}{%%
4440: \newcommand{\noopsort}[1]{}\hyphenation{ Ba-gna-ra Bie-li-ko-va Bruy-noo-ghe
4441: Common-Loops DeMich-iel Dober-kat Di-par-ti-men-to Er-vier Fa-la-schi
4442: Fell-eisen Gam-ma Gem-Stone Glan-ville Gold-in Goos-sens Graph-Trace
4443: Grim-shaw Her-men-e-gil-do Hoeks-ma Hor-o-witz Kam-i-ko Kenn-e-dy Kess-ler
4444: Lisp-edit Lu-ba-chev-sky Ma-te-ma-ti-ca Nich-o-las Obern-dorf Ohsen-doth
4445: Par-log Para-sight Pega-Sys Pren-tice Pu-ru-sho-tha-man Ra-guid-eau Rich-ard
4446: Roe-ver Ros-en-krantz Ru-dolph SIG-OA SIG-PLAN SIG-SOFT SMALL-TALK Schee-vel
4447: Schlotz-hauer Schwartz-bach Sieg-fried Small-talk Spring-er Stroh-meier
4448: Thing-Lab Zhong-xiu Zac-ca-gni-ni Zaf-fa-nel-la Zo-lo }
4449: \begin{thebibliography}{100}
4450: \expandafter\ifx\csname url\endcsname\relax
4451: \def\url#1{\texttt{#1}}\fi
4452: \expandafter\ifx\csname urlprefix\endcsname\relax\def\urlprefix{URL }\fi
4453:
4454: \bibitem{AlefeldH83}
4455: G.~Alefeld, J.~Herzberger, Introduction to Interval Computation, Academic
4456: Press, New York, 1983.
4457:
4458: \bibitem{AllenK85}
4459: J.~F. Allen, H.~A. Kautz, A model of naive temporal reasoning, in: J.~R. Hobbs,
4460: R.~Moore (eds.), Formal Theories of the Commonsense World, Ablex, Norwood,
4461: NJ, 1985, pp. 251--268.
4462:
4463: \bibitem{AlurCHHHNOSY95}
4464: R.~Alur, C.~Courcoubetis, N.~Halbwachs, T.~A. Henzinger, P.-H. Ho, X.~Nicollin,
4465: A.~Olivero, J.~Sifakis, S.~Yovine, The algorithmic analysis of hybrid
4466: systems, Theoretical Computer Science 138 (1995) 3--34.
4467:
4468: \bibitem{AlurCHH93}
4469: R.~Alur, C.~Courcoubetis, T.~A. Henzinger, P.-H. Ho, Hybrid automata: An
4470: algorithmic approach to the specification and verification of hybrid systems,
4471: in: Hybrid Systems I, vol. 736 of Lecture Notes in Computer Science, 1993.
4472:
4473: \bibitem{Ancourt91th}
4474: C.~Ancourt, G\'en\'eration automatique de codes de transfert pour
4475: multiprocesseurs \`a m\'emoires locales, Ph.D. thesis, Universit\'e de Paris
4476: VI, Paris, France (Mar. 1991).
4477:
4478: \bibitem{Avis00}
4479: D.~Avis, {lrs}: A revised implementation of the reverse search vertex
4480: enumeration algorithm, in: G.~Kalai, G.~M. Ziegler (eds.), Polytopes ---
4481: Combinatorics and Computation, vol.~29 of Oberwolfach Seminars,
4482: {Birkh\"auser-Verlag}, 2000, pp. 177--198.
4483:
4484: \bibitem{AvisB95}
4485: D.~Avis, D.~Bremner, How good are convex hull algorithms?, in: Proceedings of
4486: the Eleventh Annual Symposium on Computational Geometry, ACM Press,
4487: Vancouver, B.C., Canada, 1995.
4488:
4489: \bibitem{Bagnara97th}
4490: R.~Bagnara, Data-flow analysis for constraint logic-based languages, Ph.D.
4491: thesis, Dipartimento di Informatica, Universit\`a di Pisa, Pisa, Italy,
4492: printed as Report TD-1/97 (Mar. 1997).
4493:
4494: \bibitem{Bagnara98SCP}
4495: R.~Bagnara, A hierarchy of constraint systems for data-flow analysis of
4496: constraint logic-based languages, Science of Computer Programming 30~(1--2)
4497: (1998) 119--155.
4498:
4499: \bibitem{BagnaraDHMZ07}
4500: R.~Bagnara, K.~Dobson, P.~M. Hill, M.~Mundell, E.~Zaffanella, Grids: A domain
4501: for analyzing the distribution of numerical values, in: G.~Puebla (ed.),
4502: Logic-based Program Synthesis and Transformation, 16th International
4503: Symposium, vol. 4407 of Lecture Notes in Computer Science, Springer-Verlag,
4504: Berlin, Venice, Italy, 2007.
4505:
4506: \bibitem{BagnaraHPZ07TR}
4507: R.~Bagnara, P.~M. Hill, A.~Pescetti, E.~Zaffanella, On the design of generic
4508: static analyzers for modern imperative languages, Tech. Rep.~{\tt
4509: arXiv:cs.PL/0703116}, Dipartimento di Matematica, Universit\`a di Parma,
4510: Italy, available from \url{http://arxiv.org/} (2007).
4511:
4512: \bibitem{BagnaraHRZ05SCP}
4513: R.~Bagnara, P.~M. Hill, E.~Ricci, E.~Zaffanella, Precise widening operators for
4514: convex polyhedra, Science of Computer Programming 58~(1--2) (2005) 28--56.
4515:
4516: \bibitem{BagnaraHZ03a}
4517: R.~Bagnara, P.~M. Hill, E.~Zaffanella, A new encoding and implementation of not
4518: necessarily closed convex polyhedra, in: M.~Leuschel, S.~Gruner, S.~{Lo
4519: Presti} (eds.), Proceedings of the 3rd Workshop on Automated Verification of
4520: Critical Systems, Southampton, UK, 2003, published as TR Number
4521: DSSE-TR-2003-2, University of Southampton.
4522:
4523: \bibitem{BagnaraHZ05FAC}
4524: R.~Bagnara, P.~M. Hill, E.~Zaffanella, Not necessarily closed convex polyhedra
4525: and the double description method, Formal Aspects of Computing 17~(2) (2005)
4526: 222--257.
4527:
4528: \bibitem{BagnaraHZ06TR}
4529: R.~Bagnara, P.~M. Hill, E.~Zaffanella, The {Parma Polyhedra Library}: Toward a
4530: complete set of numerical abstractions for the analysis and verification of
4531: hardware and software systems, Quaderno 457, Dipartimento di Matematica,
4532: Universit\`a di Parma, Italy, available at
4533: \url{http://www.cs.unipr.it/Publications/}. Also published as {\tt
4534: arXiv:cs.MS/0612085}, available from \url{http://arxiv.org/}. (2006).
4535:
4536: \bibitem{PPL-USER-0-9}
4537: R.~Bagnara, P.~M. Hill, E.~Zaffanella, The {Parma Polyhedra Library} User's
4538: Manual, Department of Mathematics, University of Parma, Parma, Italy, release
4539: 0.9 ed., available at \url{http://www.cs.unipr.it/ppl/} (Mar. 2006).
4540:
4541: \bibitem{BagnaraHZ06STTT}
4542: R.~Bagnara, P.~M. Hill, E.~Zaffanella, Widening operators for powerset domains,
4543: Software Tools for Technology Transfer 8~(4/5) (2006) 449--466. (As the
4544: figures in the journal version of this paper have been improperly printed
4545: ---rendering them useless---, we recommend that interested readers download
4546: an electronic copy from the PPL's web site at
4547: \url{http://www.cs.unipr.it/ppl/}.)
4548:
4549: \bibitem{BagnaraHZ08SCP}
4550: R.~Bagnara, P.~M. Hill, E.~Zaffanella, The {Parma Polyhedra Library}: Toward a
4551: complete set of numerical abstractions for the analysis and verification of
4552: hardware and software systems, Science of Computer ProgrammingTo appear.
4553: Journal version of \cite{BagnaraHZ06TR}.
4554:
4555: \bibitem{BagnaraRZH02}
4556: R.~Bagnara, E.~Ricci, E.~Zaffanella, P.~M. Hill, Possibly not closed convex
4557: polyhedra and the {Parma Polyhedra Library}, in: M.~V. Hermenegildo,
4558: G.~Puebla (eds.), Static Analysis: Proceedings of the 9th International
4559: Symposium, vol. 2477 of Lecture Notes in Computer Science, Springer-Verlag,
4560: Berlin, Madrid, Spain, 2002.
4561:
4562: \bibitem{BagnaraR-CZ05}
4563: R.~Bagnara, E.~Rodr{\'\i}guez-Carbonell, E.~Zaffanella, Generation of basic
4564: semi-algebraic invariants using convex polyhedra, in: C.~Hankin, I.~Siveroni
4565: (eds.), Static Analysis: Proceedings of the 12th International Symposium,
4566: vol. 3672 of Lecture Notes in Computer Science, Springer-Verlag, Berlin,
4567: London, UK, 2005.
4568:
4569: \bibitem{BalasundaramK89}
4570: V.~Balasundaram, K.~Kennedy, A technique for summarizing data access and its
4571: use in parallelism enhancing transformations, in: B.~Knobe (ed.), Proceedings
4572: of the ACM SIGPLAN'89 Conference on Programming Language Design and
4573: Implementation (PLDI), vol. 24(7) of ACM SIGPLAN Notices, ACM Press,
4574: Portland, Oregon, USA, 1989.
4575:
4576: \bibitem{BaranyF05}
4577: I.~B\'ar\'any, K.~Fukuda, A case when the union of polytopes is convex, Linear
4578: Algebra and its Applications 397 (2005) 381--388.
4579:
4580: \bibitem{Bellman57}
4581: R.~Bellman, Dynamic Programming, Princeton University Press, 1957.
4582:
4583: \bibitem{BemporadFT01}
4584: A.~Bemporad, K.~Fukuda, F.~D. Torrisi, Convexity recognition of the union of
4585: polyhedra, Computational Geometry: Theory and Applications 18~(3) (2001)
4586: 141--154.
4587:
4588: \bibitem{BenoyK97}
4589: F.~Benoy, A.~King, Inferring argument size relationships with
4590: {CLP($\mathcal{R}$)}, in: J.~P. Gallagher (ed.), Logic Program Synthesis and
4591: Transformation: Proceedings of the 6th International Workshop, vol. 1207 of
4592: Lecture Notes in Computer Science, Springer-Verlag, Berlin, Stockholm,
4593: Sweden, 1997.
4594:
4595: \bibitem{BessonJT99}
4596: F.~Besson, T.~P. Jensen, J.-P. Talpin, Polyhedral analysis for synchronous
4597: languages, in: A.~Cortesi, G.~Fil\'e (eds.), Static Analysis: Proceedings of
4598: the 6th International Symposium, vol. 1694 of Lecture Notes in Computer
4599: Science, Springer-Verlag, Berlin, Venice, Italy, 1999.
4600:
4601: \bibitem{Birkhoff67}
4602: G.~Birkhoff, Lattice Theory, vol. XXV of Colloquium Publications, 3rd ed.,
4603: American Mathematical Society, Providence, Rhode Island, USA, 1967.
4604:
4605: \bibitem{BlanchetCCFMMMR03}
4606: B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
4607: D.~Monniaux, X.~Rival, A static analyzer for large safety-critical software,
4608: in: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language
4609: Design and Implementation (PLDI'03), ACM Press, San Diego, California, USA,
4610: 2003.
4611:
4612: \bibitem{BultanGP99}
4613: T.~Bultan, R.~Gerber, W.~Pugh, Model-checking concurrent systems with unbounded
4614: integer variables: Symbolic representations, approximations, and experimental
4615: results, ACM Transactions on Programming Languages and Systems 21~(4) (1999)
4616: 747--789.
4617:
4618: \bibitem{Chernikova64}
4619: N.~V. Chernikova, Algorithm for finding a general formula for the non-negative
4620: solutions of system of linear equations, U.S.S.R. Computational Mathematics
4621: and Mathematical Physics 4~(4) (1964) 151--158.
4622:
4623: \bibitem{Chernikova65}
4624: N.~V. Chernikova, Algorithm for finding a general formula for the non-negative
4625: solutions of system of linear inequalities, U.S.S.R. Computational
4626: Mathematics and Mathematical Physics 5~(2) (1965) 228--233.
4627:
4628: \bibitem{Chernikova68}
4629: N.~V. Chernikova, Algorithm for discovering the set of all solutions of a
4630: linear programming problem, U.S.S.R. Computational Mathematics and
4631: Mathematical Physics 8~(6) (1968) 282--293.
4632:
4633: \bibitem{ColonS01}
4634: M.~A. Col\'on, H.~B. Sipma, Synthesis of linear ranking functions, in:
4635: T.~Margaria, W.~Yi (eds.), Tools and Algorithms for Construction and Analysis
4636: of Systems, 7th International Conference, TACAS 2001, vol. 2031 of Lecture
4637: Notes in Computer Science, Springer-Verlag, Berlin, Genova, Italy, 2001.
4638:
4639: \bibitem{CortesiLCVH00}
4640: A.~Cortesi, B.~{Le Charlier}, P.~{Van Hentenryck}, Combinations of abstract
4641: domains for logic programming: Open product and generic pattern construction,
4642: Science of Computer Programming 38~(1--3) (2000) 27--71.
4643:
4644: \bibitem{Cousot81}
4645: P.~Cousot, Semantic foundations of program analysis, in: S.~S. Muchnick, N.~D.
4646: Jones (eds.), Program Flow Analysis: Theory and Applications, chap.~10,
4647: Prentice Hall, Englewood Cliffs, NJ, USA, 1981, pp. 303--342.
4648:
4649: \bibitem{Cousot05}
4650: P.~Cousot, Proving program invariance and termination by parametric
4651: abstraction, lagrangian relaxation and semidefinite programming, in:
4652: R.~Cousot (ed.), Verification, Model Checking and Abstract Interpretation:
4653: Proceedings of the 6th International Conference (VMCAI 2005), vol. 3385 of
4654: Lecture Notes in Computer Science, Springer-Verlag, Berlin, Paris, France,
4655: 2005.
4656:
4657: \bibitem{CousotC76}
4658: P.~Cousot, R.~Cousot, Static determination of dynamic properties of programs,
4659: in: B.~Robinet (ed.), Proceedings of the Second International Symposium on
4660: Programming, Dunod, Paris, France, Paris, France, 1976.
4661:
4662: \bibitem{CousotC77}
4663: P.~Cousot, R.~Cousot, Abstract interpretation: A unified lattice model for
4664: static analysis of programs by construction or approximation of fixpoints,
4665: in: Proceedings of the Fourth Annual ACM Symposium on Principles of
4666: Programming Languages, ACM Press, New York, 1977.
4667:
4668: \bibitem{CousotC79}
4669: P.~Cousot, R.~Cousot, Systematic design of program analysis frameworks, in:
4670: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming
4671: Languages, ACM Press, New York, 1979.
4672:
4673: \bibitem{CousotC92fr}
4674: P.~Cousot, R.~Cousot, Abstract interpretation frameworks, Journal of Logic and
4675: Computation 2~(4) (1992) 511--547.
4676:
4677: \bibitem{CousotC92plilp}
4678: P.~Cousot, R.~Cousot, Comparing the {Galois} connection and widening/narrowing
4679: approaches to abstract interpretation, in: M.~Bruynooghe, M.~Wirsing (eds.),
4680: Proceedings of the 4th International Symposium on Programming Language
4681: Implementation and Logic Programming, vol. 631 of Lecture Notes in Computer
4682: Science, Springer-Verlag, Berlin, Leuven, Belgium, 1992.
4683:
4684: \bibitem{CousotC92}
4685: P.~Cousot, R.~Cousot, Inductive definitions, semantics and abstract
4686: interpretation, in: Proceedings of the Nineteenth Annual ACM Symposium on
4687: Principles of Programming Languages, ACM Press, Albuquerque, New Mexico, USA,
4688: 1992.
4689:
4690: \bibitem{CousotH78}
4691: P.~Cousot, N.~Halbwachs, Automatic discovery of linear restraints among
4692: variables of a program, in: Conference Record of the Fifth Annual ACM
4693: Symposium on Principles of Programming Languages, ACM Press, Tucson, Arizona,
4694: 1978.
4695:
4696: \bibitem{DangDM04}
4697: T.~Dang, A.~Donz{\'e}, O.~Maler, Verification of analog and mixed-signal
4698: circuits using hybrid system techniques, in: A.~J. Hu, A.~K. Martin (eds.),
4699: Proceedings of the 5th International Conference on Formal Methods in
4700: Computer-Aided Design, vol. 3312 of Lecture Notes in Computer Science,
4701: Springer-Verlag, Berlin, Austin, Texas, USA, 2004.
4702:
4703: \bibitem{Davis87}
4704: E.~Davis, Constraint propagation with interval labels, Artificial Intelligence
4705: 32~(3) (1987) 281--331.
4706:
4707: \bibitem{DelzannoP99}
4708: G.~Delzanno, A.~Podelski, Model checking in {CLP}, in: R.~Cleaveland (ed.),
4709: Tools and Algorithms for Construction and Analysis of Systems, 5th
4710: International Conference, TACAS '99, vol. 1579 of Lecture Notes in Computer
4711: Science, Springer-Verlag, Berlin, Amsterdam, The Netherlands, 1999.
4712:
4713: \bibitem{Dill89}
4714: D.~L. Dill, Timing assumptions and verification of finite-state concurrent
4715: systems, in: J.~Sifakis (ed.), Proceedings of the International Workshop on
4716: Automatic Verification Methods for Finite State Systems, vol. 407 of Lecture
4717: Notes in Computer Science, Springer-Verlag, Berlin, Grenoble, France, 1989.
4718:
4719: \bibitem{DooseM05}
4720: D.~Doose, Z.~Mammeri, Polyhedra-based approach for incremental validation of
4721: real-time systems, in: L.~T. Yang, M.~Amamiya, Z.~Liu, M.~Guo, F.~J. Rammig
4722: (eds.), Proceedings of the International Conference on Embedded and
4723: Ubiquitous Computing (EUC 2005), vol. 3824 of Lecture Notes in Computer
4724: Science, Springer-Verlag, Berlin, Nagasaki, Japan, 2005.
4725:
4726: \bibitem{DorRS01}
4727: N.~Dor, M.~Rodeh, S.~Sagiv, Cleanness checking of string manipulations in {C}
4728: programs via integer analysis, in: P.~Cousot (ed.), Static Analysis: 8th
4729: International Symposium, SAS 2001, vol. 2126 of Lecture Notes in Computer
4730: Science, Springer-Verlag, Berlin, Paris, France, 2001.
4731:
4732: \bibitem{DoyenHR05}
4733: L.~Doyen, T.~A. Henzinger, J.-F. Raskin, Automatic rectangular refinement of
4734: affine hybrid systems, in: P.~Pettersson, W.~Yi (eds.), Proceedings of the
4735: 3rd International Conference on Formal Modeling and Analysis of Timed Systems
4736: (FORMATS 2005), vol. 3829 of Lecture Notes in Computer Science,
4737: Springer-Verlag, Berlin, Uppsala, Sweden, 2005.
4738:
4739: \bibitem{Ellenbogen04th}
4740: R.~Ellenbogen, Fully automatic verification of absence of errors via
4741: interprocedural integer analysis, Master's thesis, School of Computer
4742: Science, Tel-Aviv University, Tel-Aviv, Israel (Dec. 2004).
4743:
4744: \bibitem{Frehse04}
4745: G.~Frehse, Compositional verification of hybrid systems with discrete
4746: interaction using simulation relations, in: Proceedings of the IEEE
4747: Conference on Computer Aided Control Systems Design (CACSD 2004), Taipei,
4748: Taiwan, 2004.
4749:
4750: \bibitem{Frehse05}
4751: G.~Frehse, {PHAVer}: Algorithmic verification of hybrid systems past {HyTech},
4752: in: M.~Morari, L.~Thiele (eds.), Hybrid Systems: Computation and Control:
4753: Proceedings of the 8th International Workshop (HSCC 2005), vol. 3414 of
4754: Lecture Notes in Computer Science, Springer-Verlag, Berlin, Z{\"u}rich,
4755: Switzerland, 2005.
4756:
4757: \bibitem{FrehseHK04}
4758: G.~Frehse, Z.~Han, B.~Krogh, Assume-guarantee reasoning for hybrid
4759: {I/O}-automata by over-approximation of continuous interaction, in:
4760: Proceedings of the 43rd IEEE Conference on Decision and Control (CDC 2004),
4761: Atlantis, Paradise Island, Bahamas, 2004.
4762:
4763: \bibitem{FrehseKR06}
4764: G.~Frehse, B.~H. Krogh, R.~A. Rutenbar, Verifying analog oscillator circuits
4765: using forward/backward refinement, in: Proceedings of the 9th Conference on
4766: Design, Automation and Test in Europe (DATE 06), ACM SIGDA, Munich, Germany,
4767: 2006, {CD-ROM} publication.
4768:
4769: \bibitem{FrehseKRM06}
4770: G.~Frehse, B.~H. Krogh, R.~A. Rutenbar, O.~Maler, Time domain verification of
4771: oscillator circuit properties, in: Proceedings of the First Workshop on
4772: Formal Verification of Analog Circuits (FAC 2005), vol. 153 of Electronic
4773: Notes in Theoretical Computer Science, Elsevier Science B.V., Edinburgh,
4774: Scotland, 2006.
4775:
4776: \bibitem{FukudaP96}
4777: K.~Fukuda, A.~Prodon, Double description method revisited, in: M.~Deza,
4778: R.~Euler, Y.~Manoussakis (eds.), Combinatorics and Computer Science, 8th
4779: Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3-5,
4780: 1995, Selected Papers, vol. 1120 of Lecture Notes in Computer Science,
4781: Springer-Verlag, Berlin, 1996.
4782:
4783: \bibitem{GobertLC07}
4784: F.~Gobert, B.~{Le Charlier}, A system to check operational properties of logic
4785: programs, in: M.-L. Potet, P.-Y. Schobbens, H.~Toussaint, G.~Saval (eds.),
4786: Approches Formelles dans l'Assistance au D\'eveloppement de Logiciels: Actes
4787: de la 8e conf\'erence, Universit\'e de Namur, Belgium, 2007.
4788:
4789: \bibitem{GopanRS05}
4790: D.~Gopan, T.~W. Reps, M.~Sagiv, A framework for numeric analysis of array
4791: operations, in: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on
4792: Principles of Programming Languages, Long Beach, California, USA, 2005.
4793:
4794: \bibitem{Granger91}
4795: P.~Granger, Static analysis of linear congruence equalities among variables of
4796: a program, in: S.~Abramsky, T.~S.~E. Maibaum (eds.), TAPSOFT'91: Proceedings
4797: of the International Joint Conference on Theory and Practice of Software
4798: Development, Volume 1: Colloquium on Trees in Algebra and Programming
4799: (CAAP'91), vol. 493 of Lecture Notes in Computer Science, Springer-Verlag,
4800: Berlin, Brighton, UK, 1991.
4801:
4802: \bibitem{Granger92}
4803: P.~Granger, Improving the results of static analyses programs by local
4804: decreasing iteration, in: R.~K. Shyamasundar (ed.), Proceedings of the 12th
4805: Conference on Foundations of Software Technology and Theoretical Computer
4806: Science, vol. 652 of Lecture Notes in Computer Science, Springer-Verlag,
4807: Berlin, New Delhi, India, 1992.
4808:
4809: \bibitem{Granger97}
4810: P.~Granger, Static analyses of congruence properties on rational numbers
4811: (extended abstract), in: P.~{Van Hentenryck} (ed.), Static Analysis:
4812: Proceedings of the 4th International Symposium, vol. 1302 of Lecture Notes in
4813: Computer Science, Springer-Verlag, Berlin, Paris, France, 1997.
4814:
4815: \bibitem{GulavaniR06}
4816: B.~S. Gulavani, S.~K. Rajamani, Counterexample driven refinement for abstract
4817: interpretation, in: H.~Hermanns, J.~Palsberg (eds.), Proceedings of the 12th
4818: International Conference on Tools and Algorithms for the Construction and
4819: Analysis of Systems (TACAS 2006), vol. 3920 of Lecture Notes in Computer
4820: Science, Springer-Verlag, Berlin, Vienna, Austria, 2006.
4821:
4822: \bibitem{GuptaKR04}
4823: S.~Gupta, B.~H. Krogh, R.~A. Rutenbar, Towards formal verification of analog
4824: designs, in: Proceedings of the 2004 International Conference on
4825: Computer-Aided Design, IEEE Computer Society / ACM, San Jose, CA, USA, 2004.
4826:
4827: \bibitem{Halbwachs79th}
4828: N.~Halbwachs, D\'etermination automatique de relations lin\'eaires
4829: v\'erifi\'ees par les variables d'un programme, {Th\`ese de
4830: 3\textsuperscript{\`eme} cycle d'informatique}, Universit\'e scientifique et
4831: m\'edicale de Grenoble, Grenoble, France (Mar. 1979).
4832:
4833: \bibitem{Halbwachs93}
4834: N.~Halbwachs, Delay analysis in synchronous programs, in: C.~Courcoubetis
4835: (ed.), Computer Aided Verification: Proceedings of the 5th International
4836: Conference, vol. 697 of Lecture Notes in Computer Science, Springer-Verlag,
4837: Berlin, Elounda, Greece, 1993.
4838:
4839: \bibitem{HalbwachsMG06}
4840: N.~Halbwachs, D.~Merchat, L.~Gonnord, Some ways to reduce the space dimension
4841: in polyhedra computations, Formal Methods in System Design 29~(1) (2006)
4842: 79--95.
4843:
4844: \bibitem{HalbwachsMP-V03}
4845: N.~Halbwachs, D.~Merchat, C.~Parent-Vigouroux, Cartesian factoring of polyhedra
4846: in linear relation analysis, in: R.~Cousot (ed.), Static Analysis:
4847: Proceedings of the 10th International Symposium, vol. 2694 of Lecture Notes
4848: in Computer Science, Springer-Verlag, Berlin, San Diego, California, USA,
4849: 2003.
4850:
4851: \bibitem{HalbwachsPR94}
4852: N.~Halbwachs, Y.-E. Proy, P.~Raymond, Verification of linear hybrid systems by
4853: means of convex approximations, in: B.~{Le Charlier} (ed.), Static Analysis:
4854: Proceedings of the 1st International Symposium, vol. 864 of Lecture Notes in
4855: Computer Science, Springer-Verlag, Berlin, Namur, Belgium, 1994.
4856:
4857: \bibitem{HalbwachsPR97}
4858: N.~Halbwachs, Y.-E. Proy, P.~Roumanoff, Verification of real-time systems using
4859: linear relation analysis, Formal Methods in System Design 11~(2) (1997)
4860: 157--185.
4861:
4862: \bibitem{HartongHB02}
4863: W.~Hartong, L.~Hedrich, E.~Barke, On discrete modeling and model checking for
4864: nonlinear analog systems, in: E.~Brinksma, K.~G. Larsen (eds.), Computer
4865: Aided Verification: Proceedings of the 14th International Conference, vol.
4866: 2404 of Lecture Notes in Computer Science, Springer-Verlag, Berlin,
4867: Copenhagen, Denmark, 2002.
4868:
4869: \bibitem{HenriksenG06}
4870: K.~S. Henriksen, J.~P. Gallagher, Abstract interpretation of {PIC} programs
4871: through logic programming, in: Proceedings of the 6th IEEE International
4872: Workshop on Source Code Analysis and Manipulation, IEEE Computer Society
4873: Press, Sheraton Society Hill, Philadelphia, PA, USA, 2006.
4874:
4875: \bibitem{Henzinger96}
4876: T.~A. Henzinger, The theory of hybrid automata, in: Proceedings of the 11th
4877: Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society
4878: Press, 1996.
4879:
4880: \bibitem{HenzingerH95b}
4881: T.~A. Henzinger, P.-H. Ho, Algorithmic analysis of nonlinear hybrid systems,
4882: in: P.~Wolper (ed.), Computer Aided Verification: Proceedings of the 7th
4883: International Conference, vol. 939 of Lecture Notes in Computer Science,
4884: Springer-Verlag, Berlin, Li\`ege, Belgium, 1995.
4885:
4886: \bibitem{HenzingerH95}
4887: T.~A. Henzinger, P.-H. Ho, A note on abstract interpretation strategies for
4888: hybrid automata, in: P.~J. Antsaklis, W.~Kohn, A.~Nerode, S.~Sastry (eds.),
4889: Hybrid Systems II, vol. 999 of Lecture Notes in Computer Science,
4890: Springer-Verlag, Berlin, 1995.
4891:
4892: \bibitem{HenzingerHW97b}
4893: T.~A. Henzinger, P.-H. Ho, H.~Wong-Toi, {\sc HyTech}: A model checker for
4894: hybrid systems, Software Tools for Technology Transfer 1~(1+2) (1997)
4895: 110--122.
4896:
4897: \bibitem{HenzingerPW01}
4898: T.~A. Henzinger, J.~Preussig, H.~Wong-Toi, Some lessons from the {\sc hytech}
4899: experience, in: Proceedings of the 40th Annual Conference on Decision and
4900: Control, IEEE Computer Society Press, 2001.
4901:
4902: \bibitem{HymansU04}
4903: C.~Hymans, E.~Upton, Static analysis of gated data dependence graphs, in:
4904: R.~Giacobazzi (ed.), Static Analysis: Proceedings of the 11th International
4905: Symposium, vol. 3148 of Lecture Notes in Computer Science, Springer-Verlag,
4906: Berlin, Verona, Italy, 2004.
4907:
4908: \bibitem{Kahn87}
4909: G.~Kahn, Natural semantics, in: F.-J. Brandenburg, G.~Vidal-Naquet, M.~Wirsing
4910: (eds.), Proceedings of the 4th Annual Symposium on Theoretical Aspects of
4911: Computer Science, vol. 247 of Lecture Notes in Computer Science,
4912: Springer-Verlag, Berlin, Passau, Germany, 1987.
4913:
4914: \bibitem{Karr76}
4915: M.~Karr, Affine relationships among variables of a program, Acta Informatica 6
4916: (1976) 133--151.
4917:
4918: \bibitem{KrishnanM06}
4919: K.~Krishnan, J.~Mitchell, A unifying framework for several cutting plane
4920: methods for semidefinite programming, Optimization Methods and Software
4921: 21~(1) (2006) 57--74.
4922:
4923: \bibitem{KruegelKMRV05}
4924: C.~Kruegel, E.~Kirda, D.~Mutz, W.~Robertson, G.~Vigna, Automating mimicry
4925: attacks using static binary analysis, in: Proceedings of Security~'05, the
4926: 14th USENIX Security Symposium, Baltimore, MD, USA, 2005.
4927:
4928: \bibitem{LarsenLPY97}
4929: K.~Larsen, F.~Larsson, P.~Pettersson, W.~Yi, Efficient verification of
4930: real-time systems: Compact data structure and state-space reduction, in:
4931: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS'97), IEEE
4932: Computer Society Press, San Francisco, CA, 1997.
4933:
4934: \bibitem{LassezM92}
4935: J.-L. Lassez, M.~J. Maher, On {F}ourier's algorithm for linear arithmetic
4936: constraints, J. Autom. Reasoning 9~(3) (1992) 373--379.
4937:
4938: \bibitem{LeVerge92}
4939: H.~{Le Verge}, A note on {Chernikova's} algorithm, \emph{Publication interne}
4940: 635, IRISA, Campus de Beaulieu, Rennes, France (1992).
4941:
4942: \bibitem{Leroy06}
4943: X.~Leroy, Coinductive big-step operational semantics, in: P.~Sestoft (ed.),
4944: Programming Languages and Systems, Proceedings of the 14th European Symposium
4945: on Programming, vol. 3924 of Lecture Notes in Computer Science,
4946: Springer-Verlag, Berlin, Vienna, Austria, 2006.
4947:
4948: \bibitem{Loechner99}
4949: V.~Loechner, {\it PolyLib\/}: A library for manipulating parameterized
4950: polyhedra, Available at \url{http://icps.u-strasbg.fr/~loechner/polylib/},
4951: declares itself to be a continuation of \cite{Wilde93th} (Mar. 1999).
4952:
4953: \bibitem{Maler06}
4954: O.~Maler, Analog circuit verification: A state of an art, in: Proceedings of
4955: the First Workshop on Formal Verification of Analog Circuits (FAC 2005), vol.
4956: 153 of Electronic Notes in Theoretical Computer Science, Elsevier Science
4957: B.V., Edinburgh, Scotland, 2006.
4958:
4959: \bibitem{MesnardB05TPLP}
4960: F.~Mesnard, R.~Bagnara, {cTI}: A constraint-based termination inference tool
4961: for {ISO-Prolog}, Theory and Practice of Logic Programming 5~(1{\&}2) (2005)
4962: 243--257.
4963:
4964: \bibitem{Mine01b}
4965: A.~Min\'e, The octagon abstract domain, in: Proceedings of the Eighth Working
4966: Conference on Reverse Engineering (WCRE'01), IEEE Computer Society Press,
4967: Stuttgart, Germany, 2001.
4968:
4969: \bibitem{Mine05th}
4970: A.~Min\'e, Weakly relational numerical abstract domains, Ph.D. thesis, \'Ecole
4971: Polytechnique, Paris, France (Mar. 2005).
4972:
4973: \bibitem{MotzkinRTT53}
4974: T.~S. Motzkin, H.~Raiffa, G.~L. Thompson, R.~M. Thrall, The double description
4975: method, in: H.~W. Kuhn, A.~W. Tucker (eds.), Contributions to the Theory of
4976: Games -- Volume II, No.~28 in Annals of Mathematics Studies, Princeton
4977: University Press, Princeton, New Jersey, 1953, pp. 51--73.
4978:
4979: \bibitem{MullerS00}
4980: O.~M\"{u}ller, T.~Stauner, Modelling and verification using linear hybrid
4981: systems, Mathematical and Computer Modelling of Dynamical Systems 6~(1)
4982: (2000) 71--89.
4983:
4984: \bibitem{Muller-OlmS04ICALP}
4985: M.~{M\"uller-Olm}, H.~Seidl, A note on {Karr's} algorithm, in: J.~Diaz,
4986: J.~{Karhum\"aki}, A.~et~al. (eds.), Automata, Languages and Programming:
4987: Proceedings of the 31st International Colloquium (ICALP 2004), vol. 3142 of
4988: Lecture Notes in Computer Science, Springer-Verlag, Berlin, Turku, Finland,
4989: 2004.
4990:
4991: \bibitem{NakanishiJPF99}
4992: T.~Nakanishi, K.~Joe, C.~D. Polychronopoulos, A.~Fukuda, The modulo interval: A
4993: simple and practical representation for program analysis, in: Proceedings of
4994: the 1999 International Conference on Parallel Architectures and Compilation
4995: Techniques, IEEE Computer Society, Newport Beach, California, USA, 1999.
4996:
4997: \bibitem{NookalaR00}
4998: S.~P.~K. Nookala, T.~Risset, A library for {Z}-polyhedral operations,
4999: \emph{Publication interne} 1330, IRISA, Campus de Beaulieu, Rennes, France
5000: (2000).
5001:
5002: \bibitem{Plotkin81}
5003: G.~Plotkin, A structural approach to operational semantics, Tech. Rep. DAIMI
5004: FN-19, Computer Science Department, University of Aarhus, Denmark (1981).
5005:
5006: \bibitem{QuintonRR96}
5007: P.~Quinton, S.~Rajopadhye, T.~Risset, On manipulating {Z}-polyhedra, Tech. Rep.
5008: 1016, IRISA, Campus Universitaire de Bealieu, Rennes, France (Jul. 1996).
5009:
5010: \bibitem{SankaranarayananCSM06}
5011: S.~Sankaranarayanan, M.~Col{\'o}n, H.~B. Sipma, Z.~Manna, Efficient strongly
5012: relational polyhedral analysis, in: E.~A. Emerson, K.~S. Namjoshi (eds.),
5013: Verification, Model Checking and Abstract Interpretation: Proceedings of the
5014: 7th International Conference (VMCAI 2006), vol. 3855 of Lecture Notes in
5015: Computer Science, Springer-Verlag, Berlin, Charleston, SC, USA, 2006.
5016:
5017: \bibitem{SankaranarayananSM05}
5018: S.~Sankaranarayanan, H.~B. Sipma, Z.~Manna, Scalable analysis of linear systems
5019: using mathematical programming, in: R.~Cousot (ed.), Verification, Model
5020: Checking and Abstract Interpretation: Proceedings of the 6th International
5021: Conference (VMCAI 2005), vol. 3385 of Lecture Notes in Computer Science,
5022: Springer-Verlag, Berlin, Paris, France, 2005.
5023:
5024: \bibitem{SankaranarayananSM06}
5025: S.~Sankaranarayanan, H.~B. Sipma, Z.~Manna, Fixed point iteration for computing
5026: the time elapse operator, in: J.~Hespanha, A.~Tiwari (eds.), Hybrid Systems:
5027: Computation and Control: Proceedings of the 9th International Workshop (HSCC
5028: 2006), vol. 3927 of Lecture Notes in Computer Science, Springer-Verlag,
5029: Berlin, Santa Barbara, CA, USA, 2006.
5030:
5031: \bibitem{Schmidt95}
5032: D.~A. Schmidt, Natural-semantics-based abstract interpretation (preliminary
5033: version), in: A.~Mycroft (ed.), Static Analysis: Proceedings of the 2nd
5034: International Symposium, vol. 983 of Lecture Notes in Computer Science,
5035: Springer-Verlag, Berlin, Glasgow, UK, 1995.
5036:
5037: \bibitem{Schmidt97}
5038: D.~A. Schmidt, Abstract interpretation of small-step semantics, in: M.~Dam
5039: (ed.), Analysis and Verification of Multiple-Agent Languages, vol. 1192 of
5040: Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1997, pp. 76--99,
5041: 5th LOMAPS Workshop Stockholm, Sweden, June 24--26, 1996, Selected Papers.
5042:
5043: \bibitem{Schmidt98}
5044: D.~A. Schmidt, Trace-based abstract interpretation of operational semantics,
5045: {LISP} and Symbolic Computation 10~(3) (1998) 237--271.
5046:
5047: \bibitem{Schrijver99}
5048: A.~Schrijver, Theory of Linear and Integer Programming, Wiley Interscience
5049: Series in Discrete Mathematics and Optimization, John Wiley \& Sons, 1999.
5050:
5051: \bibitem{ShahamKS00}
5052: R.~Shaham, E.~K. Kolodner, S.~Sagiv, Automatic removal of array memory leaks in
5053: {J}ava, in: D.~A. Watt (ed.), Proceedings of the 9th International Conference
5054: on Compiler Construction (CC 2000), vol. 1781 of Lecture Notes in Computer
5055: Science, Springer-Verlag, Berlin, Berlin, Germany, 2000.
5056:
5057: \bibitem{SimonKH02}
5058: A.~Simon, A.~King, J.~M. Howe, Two variables per linear inequality as an
5059: abstract domain, in: M.~Leuschel (ed.), Logic Based Program Synthesis and
5060: Tranformation, 12th International Workshop, vol. 2664 of Lecture Notes in
5061: Computer Science, Springer-Verlag, Berlin, Madrid, Spain, 2002.
5062:
5063: \bibitem{SohnVG91}
5064: K.~Sohn, A.~{Van Gelder}, Termination detection in logic programs using
5065: argument sizes (extended abstract), in: Proceedings of the Tenth {ACM}
5066: {SIGACT-SIGMOD-SIGART} Symposium on Principles of Database Systems, ACM,
5067: Association for Computing Machinery, Denver, Colorado, United States, 1991.
5068:
5069: \bibitem{SongCR06}
5070: H.~Song, K.~J. Compton, W.~C. Rounds, {SPHIN:} a model checker for
5071: reconfigurable hybrid systems based on {SPIN}, in: R.~Lazic, R.~Nagarajan
5072: (eds.), Proceedings of the 5th International Workshop on Automated
5073: Verification of Critical Systems, vol. 145 of Electronic Notes in Theoretical
5074: Computer Science, University of Warwick, UK, 2006.
5075:
5076: \bibitem{StoerW70}
5077: J.~Stoer, C.~Witzgall, Convexity and Optimization in Finite Dimensions {I},
5078: Springer-Verlag, Berlin, 1970.
5079:
5080: \bibitem{vanHeeOSV06}
5081: K.~{van Hee}, O.~Oanea, N.~Sidorova, M.~Voorhoeve, Verifying generalized
5082: soundness for workflow nets, in: I.~Virbitskaite, A.~Voronkov (eds.),
5083: Perspectives of System Informatics: Proceedings of the Sixth International
5084: Andrei Ershov Memorial Conference, vol. 4378 of Lecture Notes in Computer
5085: Science, Springer-Verlag, Berlin, Akademgorodok, Novosibirsk, Russia, 2006.
5086:
5087: \bibitem{VenetB04}
5088: A.~Venet, G.~Brat, Precise and efficient static array bound checking for large
5089: embedded {C} programs, in: Proceedings of the ACM SIGPLAN 2004 Conference on
5090: Programming Language Design and Implementation (PLDI'04), ACM Press,
5091: Washington, DC, USA, 2004.
5092:
5093: \bibitem{Wilde93th}
5094: D.~K. Wilde, A library for doing polyhedral operations, {Master's thesis},
5095: Oregon State University, Corvallis, Oregon, also published as IRISA
5096: \emph{Publication interne} 785, Rennes, France, 1993 (Dec. 1993).
5097:
5098: \end{thebibliography}
5099: }{%%
5100: \newcommand{\noopsort}[1]{}\hyphenation{ Ba-gna-ra Bie-li-ko-va Bruy-noo-ghe
5101: Common-Loops DeMich-iel Dober-kat Di-par-ti-men-to Er-vier Fa-la-schi
5102: Fell-eisen Gam-ma Gem-Stone Glan-ville Gold-in Goos-sens Graph-Trace
5103: Grim-shaw Her-men-e-gil-do Hoeks-ma Hor-o-witz Kam-i-ko Kenn-e-dy Kess-ler
5104: Lisp-edit Lu-ba-chev-sky Ma-te-ma-ti-ca Nich-o-las Obern-dorf Ohsen-doth
5105: Par-log Para-sight Pega-Sys Pren-tice Pu-ru-sho-tha-man Ra-guid-eau Rich-ard
5106: Roe-ver Ros-en-krantz Ru-dolph SIG-OA SIG-PLAN SIG-SOFT SMALL-TALK Schee-vel
5107: Schlotz-hauer Schwartz-bach Sieg-fried Small-talk Spring-er Stroh-meier
5108: Thing-Lab Zhong-xiu Zac-ca-gni-ni Zaf-fa-nel-la Zo-lo }
5109: \begin{thebibliography}{10}
5110: \expandafter\ifx\csname url\endcsname\relax
5111: \def\url#1{\texttt{#1}}\fi
5112: \expandafter\ifx\csname urlprefix\endcsname\relax\def\urlprefix{URL }\fi
5113:
5114: \bibitem{AlefeldH83}
5115: G.~Alefeld, J.~Herzberger, Introduction to Interval Computation, Academic
5116: Press, New York, 1983.
5117:
5118: \bibitem{AlurCHH93}
5119: R.~Alur, C.~Courcoubetis, T.~A. Henzinger, P.-H. Ho, Hybrid automata: An
5120: algorithmic approach to the specification and verification of hybrid systems,
5121: in: Hybrid Systems I, vol. 736 of Lecture Notes in Computer Science, 1993.
5122:
5123: \bibitem{Ancourt91th}
5124: C.~Ancourt, G\'en\'eration automatique de codes de transfert pour
5125: multiprocesseurs \`a m\'emoires locales, Ph.D. thesis, Universit\'e de Paris
5126: VI, Paris, France (Mar. 1991).
5127:
5128: \bibitem{Avis00}
5129: D.~Avis, {lrs}: A revised implementation of the reverse search vertex
5130: enumeration algorithm, in: G.~Kalai, G.~M. Ziegler (eds.), Polytopes ---
5131: Combinatorics and Computation, vol.~29 of Oberwolfach Seminars,
5132: {Birkh\"auser-Verlag}, 2000, pp. 177--198.
5133:
5134: \bibitem{AvisB95}
5135: D.~Avis, D.~Bremner, How good are convex hull algorithms?, in: Proceedings of
5136: the Eleventh Annual Symposium on Computational Geometry, ACM Press,
5137: Vancouver, B.C., Canada, 1995.
5138:
5139: \bibitem{Bagnara97th}
5140: R.~Bagnara, Data-flow analysis for constraint logic-based languages, Ph.D.
5141: thesis, Dipartimento di Informatica, Universit\`a di Pisa, Pisa, Italy,
5142: printed as Report TD-1/97 (Mar. 1997).
5143:
5144: \bibitem{Bagnara98SCP}
5145: R.~Bagnara, A hierarchy of constraint systems for data-flow analysis of
5146: constraint logic-based languages, Science of Computer Programming 30~(1--2)
5147: (1998) 119--155.
5148:
5149: \bibitem{BagnaraDHMZ07}
5150: R.~Bagnara, K.~Dobson, P.~M. Hill, M.~Mundell, E.~Zaffanella, Grids: A domain
5151: for analyzing the distribution of numerical values, in: G.~Puebla (ed.),
5152: Logic-based Program Synthesis and Transformation, 16th International
5153: Symposium, vol. 4407 of Lecture Notes in Computer Science, Springer-Verlag,
5154: Berlin, Venice, Italy, 2007.
5155:
5156: \bibitem{BagnaraHPZ07TR}
5157: R.~Bagnara, P.~M. Hill, A.~Pescetti, E.~Zaffanella, On the design of generic
5158: static analyzers for modern imperative languages, Tech. Rep.~{\tt
5159: arXiv:cs.PL/0703116}, Dipartimento di Matematica, Universit\`a di Parma,
5160: Italy, available from \url{http://arxiv.org/} (2007).
5161:
5162: \bibitem{BagnaraHRZ05SCP}
5163: R.~Bagnara, P.~M. Hill, E.~Ricci, E.~Zaffanella, Precise widening operators for
5164: convex polyhedra, Science of Computer Programming 58~(1--2) (2005) 28--56.
5165:
5166: \bibitem{BagnaraHZ05FAC}
5167: R.~Bagnara, P.~M. Hill, E.~Zaffanella, Not necessarily closed convex polyhedra
5168: and the double description method, Formal Aspects of Computing 17~(2) (2005)
5169: 222--257.
5170:
5171: \bibitem{BagnaraHZ06STTT}
5172: R.~Bagnara, P.~M. Hill, E.~Zaffanella, Widening operators for powerset domains,
5173: Software Tools for Technology Transfer 8~(4/5) (2006) 449--466. (As the
5174: figures in the journal version of this paper have been improperly printed
5175: ---rendering them useless---, we recommend that interested readers download
5176: an electronic copy from the PPL's web site at
5177: \url{http://www.cs.unipr.it/ppl/}.)
5178:
5179: \bibitem{BagnaraHZ07TRa}
5180: R.~Bagnara, P.~M. Hill, E.~Zaffanella, Applications of polyhedral computations
5181: to the analysis and verification of hardware and software systems,
5182: {\tt arXiv:cs.CG/0701122}, available from \url{http://arxiv.org/}. (2007).
5183:
5184: \bibitem{BagnaraHZ08SCP}
5185: R.~Bagnara, P.~M. Hill, E.~Zaffanella, The {Parma Polyhedra Library}: Toward a
5186: complete set of numerical abstractions for the analysis and verification of
5187: hardware and software systems, Science of Computer ProgrammingTo appear.
5188:
5189: \bibitem{BagnaraR-CZ05}
5190: R.~Bagnara, E.~Rodr{\'\i}guez-Carbonell, E.~Zaffanella, Generation of basic
5191: semi-algebraic invariants using convex polyhedra, in: C.~Hankin, I.~Siveroni
5192: (eds.), Static Analysis: Proceedings of the 12th International Symposium,
5193: vol. 3672 of Lecture Notes in Computer Science, Springer-Verlag, Berlin,
5194: London, UK, 2005.
5195:
5196: \bibitem{Bellman57}
5197: R.~Bellman, Dynamic Programming, Princeton University Press, 1957.
5198:
5199: \bibitem{BemporadFT01}
5200: A.~Bemporad, K.~Fukuda, F.~D. Torrisi, Convexity recognition of the union of
5201: polyhedra, Computational Geometry: Theory and Applications 18~(3) (2001)
5202: 141--154.
5203:
5204: \bibitem{BenoyK97}
5205: F.~Benoy, A.~King, Inferring argument size relationships with
5206: {CLP($\mathcal{R}$)}, in: J.~P. Gallagher (ed.), Logic Program Synthesis and
5207: Transformation: Proceedings of the 6th International Workshop, vol. 1207 of
5208: Lecture Notes in Computer Science, Springer-Verlag, Berlin, Stockholm,
5209: Sweden, 1997.
5210:
5211: \bibitem{BessonJT99}
5212: F.~Besson, T.~P. Jensen, J.-P. Talpin, Polyhedral analysis for synchronous
5213: languages, in: A.~Cortesi, G.~Fil\'e (eds.), Static Analysis: Proceedings of
5214: the 6th International Symposium, vol. 1694 of Lecture Notes in Computer
5215: Science, Springer-Verlag, Berlin, Venice, Italy, 1999.
5216:
5217: \bibitem{Birkhoff67}
5218: G.~Birkhoff, Lattice Theory, vol. XXV of Colloquium Publications, 3rd ed.,
5219: American Mathematical Society, Providence, Rhode Island, USA, 1967.
5220:
5221: \bibitem{BlanchetCCFMMMR03}
5222: B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
5223: D.~Monniaux, X.~Rival, A static analyzer for large safety-critical software,
5224: in: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language
5225: Design and Implementation (PLDI'03), ACM Press, San Diego, California, USA,
5226: 2003.
5227:
5228: \bibitem{BultanGP99}
5229: T.~Bultan, R.~Gerber, W.~Pugh, Model-checking concurrent systems with unbounded
5230: integer variables: Symbolic representations, approximations, and experimental
5231: results, ACM Transactions on Programming Languages and Systems 21~(4) (1999)
5232: 747--789.
5233:
5234: \bibitem{Chernikova68}
5235: N.~V. Chernikova, Algorithm for discovering the set of all solutions of a
5236: linear programming problem, U.S.S.R. Computational Mathematics and
5237: Mathematical Physics 8~(6) (1968) 282--293.
5238:
5239: \bibitem{ColonS01}
5240: M.~A. Col\'on, H.~B. Sipma, Synthesis of linear ranking functions, in:
5241: T.~Margaria, W.~Yi (eds.), Tools and Algorithms for Construction and Analysis
5242: of Systems, 7th International Conference, TACAS 2001, vol. 2031 of Lecture
5243: Notes in Computer Science, Springer-Verlag, Berlin, Genova, Italy, 2001.
5244:
5245: \bibitem{CortesiLCVH00}
5246: A.~Cortesi, B.~{Le Charlier}, P.~{Van Hentenryck}, Combinations of abstract
5247: domains for logic programming: Open product and generic pattern construction,
5248: Science of Computer Programming 38~(1--3) (2000) 27--71.
5249:
5250: \bibitem{Cousot05}
5251: P.~Cousot, Proving program invariance and termination by parametric
5252: abstraction, lagrangian relaxation and semidefinite programming, in:
5253: R.~Cousot (ed.), Verification, Model Checking and Abstract Interpretation:
5254: Proceedings of the 6th International Conference (VMCAI 2005), vol. 3385 of
5255: Lecture Notes in Computer Science, Springer-Verlag, Berlin, Paris, France,
5256: 2005.
5257:
5258: \bibitem{CousotC76}
5259: P.~Cousot, R.~Cousot, Static determination of dynamic properties of programs,
5260: in: B.~Robinet (ed.), Proceedings of the Second International Symposium on
5261: Programming, Dunod, Paris, France, Paris, France, 1976.
5262:
5263: \bibitem{CousotC79}
5264: P.~Cousot, R.~Cousot, Systematic design of program analysis frameworks, in:
5265: Proceedings of the Sixth Annual ACM Symposium on Principles of Programming
5266: Languages, ACM Press, New York, 1979.
5267:
5268: \bibitem{CousotC92fr}
5269: P.~Cousot, R.~Cousot, Abstract interpretation frameworks, Journal of Logic and
5270: Computation 2~(4) (1992) 511--547.
5271:
5272: \bibitem{CousotC92}
5273: P.~Cousot, R.~Cousot, Inductive definitions, semantics and abstract
5274: interpretation, in: Proceedings of the Nineteenth Annual ACM Symposium on
5275: Principles of Programming Languages, ACM Press, Albuquerque, New Mexico, USA,
5276: 1992.
5277:
5278: \bibitem{CousotH78}
5279: P.~Cousot, N.~Halbwachs, Automatic discovery of linear restraints among
5280: variables of a program, in: Conference Record of the Fifth Annual ACM
5281: Symposium on Principles of Programming Languages, ACM Press, Tucson, Arizona,
5282: 1978.
5283:
5284: \bibitem{Davis87}
5285: E.~Davis, Constraint propagation with interval labels, Artificial Intelligence
5286: 32~(3) (1987) 281--331.
5287:
5288: \bibitem{DelzannoP99}
5289: G.~Delzanno, A.~Podelski, Model checking in {CLP}, in: R.~Cleaveland (ed.),
5290: Tools and Algorithms for Construction and Analysis of Systems, 5th
5291: International Conference, TACAS '99, vol. 1579 of Lecture Notes in Computer
5292: Science, Springer-Verlag, Berlin, Amsterdam, The Netherlands, 1999.
5293:
5294: \bibitem{DooseM05}
5295: D.~Doose, Z.~Mammeri, Polyhedra-based approach for incremental validation of
5296: real-time systems, in: L.~T. Yang, M.~Amamiya, Z.~Liu, M.~Guo, F.~J. Rammig
5297: (eds.), Proceedings of the International Conference on Embedded and
5298: Ubiquitous Computing (EUC 2005), vol. 3824 of Lecture Notes in Computer
5299: Science, Springer-Verlag, Berlin, Nagasaki, Japan, 2005.
5300:
5301: \bibitem{DorRS01}
5302: N.~Dor, M.~Rodeh, S.~Sagiv, Cleanness checking of string manipulations in {C}
5303: programs via integer analysis, in: P.~Cousot (ed.), Static Analysis: 8th
5304: International Symposium, SAS 2001, vol. 2126 of Lecture Notes in Computer
5305: Science, Springer-Verlag, Berlin, Paris, France, 2001.
5306:
5307: \bibitem{DoyenHR05}
5308: L.~Doyen, T.~A. Henzinger, J.-F. Raskin, Automatic rectangular refinement of
5309: affine hybrid systems, in: P.~Pettersson, W.~Yi (eds.), Proceedings of the
5310: 3rd International Conference on Formal Modeling and Analysis of Timed Systems
5311: (FORMATS 2005), vol. 3829 of Lecture Notes in Computer Science,
5312: Springer-Verlag, Berlin, Uppsala, Sweden, 2005.
5313:
5314: \bibitem{Ellenbogen04th}
5315: R.~Ellenbogen, Fully automatic verification of absence of errors via
5316: interprocedural integer analysis, Master's thesis, School of Computer
5317: Science, Tel-Aviv University, Tel-Aviv, Israel (Dec. 2004).
5318:
5319: \bibitem{Frehse05}
5320: G.~Frehse, {PHAVer}: Algorithmic verification of hybrid systems past {HyTech},
5321: in: M.~Morari, L.~Thiele (eds.), Hybrid Systems: Computation and Control:
5322: Proceedings of the 8th International Workshop (HSCC 2005), vol. 3414 of
5323: Lecture Notes in Computer Science, Springer-Verlag, Berlin, Z{\"u}rich,
5324: Switzerland, 2005.
5325:
5326: \bibitem{FrehseKR06}
5327: G.~Frehse, B.~H. Krogh, R.~A. Rutenbar, Verifying analog oscillator circuits
5328: using forward/backward refinement, in: Proceedings of the 9th Conference on
5329: Design, Automation and Test in Europe (DATE 06), ACM SIGDA, Munich, Germany,
5330: 2006, {CD-ROM} publication.
5331:
5332: \bibitem{FukudaP96}
5333: K.~Fukuda, A.~Prodon, Double description method revisited, in: M.~Deza,
5334: R.~Euler, Y.~Manoussakis (eds.), Combinatorics and Computer Science, 8th
5335: Franco-Japanese and 4th Franco-Chinese Conference, Brest, France, July 3-5,
5336: 1995, Selected Papers, vol. 1120 of Lecture Notes in Computer Science,
5337: Springer-Verlag, Berlin, 1996.
5338:
5339: \bibitem{GopanRS05}
5340: D.~Gopan, T.~W. Reps, M.~Sagiv, A framework for numeric analysis of array
5341: operations, in: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on
5342: Principles of Programming Languages, Long Beach, California, USA, 2005.
5343:
5344: \bibitem{Granger92}
5345: P.~Granger, Improving the results of static analyses programs by local
5346: decreasing iteration, in: R.~K. Shyamasundar (ed.), Proceedings of the 12th
5347: Conference on Foundations of Software Technology and Theoretical Computer
5348: Science, vol. 652 of Lecture Notes in Computer Science, Springer-Verlag,
5349: Berlin, New Delhi, India, 1992.
5350:
5351: \bibitem{Granger97}
5352: P.~Granger, Static analyses of congruence properties on rational numbers
5353: (extended abstract), in: P.~{Van Hentenryck} (ed.), Static Analysis:
5354: Proceedings of the 4th International Symposium, vol. 1302 of Lecture Notes in
5355: Computer Science, Springer-Verlag, Berlin, Paris, France, 1997.
5356:
5357: \bibitem{GulavaniR06}
5358: B.~S. Gulavani, S.~K. Rajamani, Counterexample driven refinement for abstract
5359: interpretation, in: H.~Hermanns, J.~Palsberg (eds.), Proceedings of the 12th
5360: International Conference on Tools and Algorithms for the Construction and
5361: Analysis of Systems (TACAS 2006), vol. 3920 of Lecture Notes in Computer
5362: Science, Springer-Verlag, Berlin, Vienna, Austria, 2006.
5363:
5364: \bibitem{Halbwachs93}
5365: N.~Halbwachs, Delay analysis in synchronous programs, in: C.~Courcoubetis
5366: (ed.), Computer Aided Verification: Proceedings of the 5th International
5367: Conference, vol. 697 of Lecture Notes in Computer Science, Springer-Verlag,
5368: Berlin, Elounda, Greece, 1993.
5369:
5370: \bibitem{HalbwachsMG06}
5371: N.~Halbwachs, D.~Merchat, L.~Gonnord, Some ways to reduce the space dimension
5372: in polyhedra computations, Formal Methods in System Design 29~(1) (2006)
5373: 79--95.
5374:
5375: \bibitem{HalbwachsPR97}
5376: N.~Halbwachs, Y.-E. Proy, P.~Roumanoff, Verification of real-time systems using
5377: linear relation analysis, Formal Methods in System Design 11~(2) (1997)
5378: 157--185.
5379:
5380: \bibitem{HartongHB02}
5381: W.~Hartong, L.~Hedrich, E.~Barke, On discrete modeling and model checking for
5382: nonlinear analog systems, in: E.~Brinksma, K.~G. Larsen (eds.), Computer
5383: Aided Verification: Proceedings of the 14th International Conference, vol.
5384: 2404 of Lecture Notes in Computer Science, Springer-Verlag, Berlin,
5385: Copenhagen, Denmark, 2002.
5386:
5387: \bibitem{Henzinger96}
5388: T.~A. Henzinger, The theory of hybrid automata, in: Proceedings of the 11th
5389: Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society
5390: Press, 1996.
5391:
5392: \bibitem{HenzingerH95}
5393: T.~A. Henzinger, P.-H. Ho, A note on abstract interpretation strategies for
5394: hybrid automata, in: P.~J. Antsaklis, W.~Kohn, A.~Nerode, S.~Sastry (eds.),
5395: Hybrid Systems II, vol. 999 of Lecture Notes in Computer Science,
5396: Springer-Verlag, Berlin, 1995.
5397:
5398: \bibitem{HenzingerHW97b}
5399: T.~A. Henzinger, P.-H. Ho, H.~Wong-Toi, {\sc HyTech}: A model checker for
5400: hybrid systems, Software Tools for Technology Transfer 1~(1+2) (1997)
5401: 110--122.
5402:
5403: \bibitem{HenzingerPW01}
5404: T.~A. Henzinger, J.~Preussig, H.~Wong-Toi, Some lessons from the {\sc hytech}
5405: experience, in: Proceedings of the 40th Annual Conference on Decision and
5406: Control, IEEE Computer Society Press, 2001.
5407:
5408: \bibitem{HymansU04}
5409: C.~Hymans, E.~Upton, Static analysis of gated data dependence graphs, in:
5410: R.~Giacobazzi (ed.), Static Analysis: Proceedings of the 11th International
5411: Symposium, vol. 3148 of Lecture Notes in Computer Science, Springer-Verlag,
5412: Berlin, Verona, Italy, 2004.
5413:
5414: \bibitem{Kahn87}
5415: G.~Kahn, Natural semantics, in: F.-J. Brandenburg, G.~Vidal-Naquet, M.~Wirsing
5416: (eds.), Proceedings of the 4th Annual Symposium on Theoretical Aspects of
5417: Computer Science, vol. 247 of Lecture Notes in Computer Science,
5418: Springer-Verlag, Berlin, Passau, Germany, 1987.
5419:
5420: \bibitem{Karr76}
5421: M.~Karr, Affine relationships among variables of a program, Acta Informatica 6
5422: (1976) 133--151.
5423:
5424: \bibitem{KrishnanM06}
5425: K.~Krishnan, J.~Mitchell, A unifying framework for several cutting plane
5426: methods for semidefinite programming, Optimization Methods and Software
5427: 21~(1) (2006) 57--74.
5428:
5429: \bibitem{KruegelKMRV05}
5430: C.~Kruegel, E.~Kirda, D.~Mutz, W.~Robertson, G.~Vigna, Automating mimicry
5431: attacks using static binary analysis, in: Proceedings of Security~'05, the
5432: 14th USENIX Security Symposium, Baltimore, MD, USA, 2005.
5433:
5434: \bibitem{LassezM92}
5435: J.-L. Lassez, M.~J. Maher, On {F}ourier's algorithm for linear arithmetic
5436: constraints, J. Autom. Reasoning 9~(3) (1992) 373--379.
5437:
5438: \bibitem{LeVerge92}
5439: H.~{Le Verge}, A note on {Chernikova's} algorithm, \emph{Publication interne}
5440: 635, IRISA, Campus de Beaulieu, Rennes, France (1992).
5441:
5442: \bibitem{Loechner99}
5443: V.~Loechner, {\it PolyLib\/}: A library for manipulating parameterized
5444: polyhedra, Available at \url{http://icps.u-strasbg.fr/~loechner/polylib/},
5445: declares itself to be a continuation of \cite{Wilde93th} (Mar. 1999).
5446:
5447: \bibitem{MesnardB05TPLP}
5448: F.~Mesnard, R.~Bagnara, {cTI}: A constraint-based termination inference tool
5449: for {ISO-Prolog}, Theory and Practice of Logic Programming 5~(1{\&}2) (2005)
5450: 243--257.
5451:
5452: \bibitem{Mine05th}
5453: A.~Min\'e, Weakly relational numerical abstract domains, Ph.D. thesis, \'Ecole
5454: Polytechnique, Paris, France (Mar. 2005).
5455:
5456: \bibitem{MotzkinRTT53}
5457: T.~S. Motzkin, H.~Raiffa, G.~L. Thompson, R.~M. Thrall, The double description
5458: method, in: H.~W. Kuhn, A.~W. Tucker (eds.), Contributions to the Theory of
5459: Games -- Volume II, No.~28 in Annals of Mathematics Studies, Princeton
5460: University Press, Princeton, New Jersey, 1953, pp. 51--73.
5461:
5462: \bibitem{NakanishiJPF99}
5463: T.~Nakanishi, K.~Joe, C.~D. Polychronopoulos, A.~Fukuda, The modulo interval: A
5464: simple and practical representation for program analysis, in: Proceedings of
5465: the 1999 International Conference on Parallel Architectures and Compilation
5466: Techniques, IEEE Computer Society, Newport Beach, California, USA, 1999.
5467:
5468: \bibitem{NookalaR00}
5469: S.~P.~K. Nookala, T.~Risset, A library for {Z}-polyhedral operations,
5470: \emph{Publication interne} 1330, IRISA, Campus de Beaulieu, Rennes, France
5471: (2000).
5472:
5473: \bibitem{Plotkin81}
5474: G.~Plotkin, A structural approach to operational semantics, Tech. Rep. DAIMI
5475: FN-19, Computer Science Department, University of Aarhus, Denmark (1981).
5476:
5477: \bibitem{QuintonRR96}
5478: P.~Quinton, S.~Rajopadhye, T.~Risset, On manipulating {Z}-polyhedra, Tech. Rep.
5479: 1016, IRISA, Campus Universitaire de Bealieu, Rennes, France (Jul. 1996).
5480:
5481: \bibitem{SankaranarayananCSM06}
5482: S.~Sankaranarayanan, M.~Col{\'o}n, H.~B. Sipma, Z.~Manna, Efficient strongly
5483: relational polyhedral analysis, in: E.~A. Emerson, K.~S. Namjoshi (eds.),
5484: Verification, Model Checking and Abstract Interpretation: Proceedings of the
5485: 7th International Conference (VMCAI 2006), vol. 3855 of Lecture Notes in
5486: Computer Science, Springer-Verlag, Berlin, Charleston, SC, USA, 2006.
5487:
5488: \bibitem{SankaranarayananSM05}
5489: S.~Sankaranarayanan, H.~B. Sipma, Z.~Manna, Scalable analysis of linear systems
5490: using mathematical programming, in: R.~Cousot (ed.), Verification, Model
5491: Checking and Abstract Interpretation: Proceedings of the 6th International
5492: Conference (VMCAI 2005), vol. 3385 of Lecture Notes in Computer Science,
5493: Springer-Verlag, Berlin, Paris, France, 2005.
5494:
5495: \bibitem{Schmidt95}
5496: D.~A. Schmidt, Natural-semantics-based abstract interpretation (preliminary
5497: version), in: A.~Mycroft (ed.), Static Analysis: Proceedings of the 2nd
5498: International Symposium, vol. 983 of Lecture Notes in Computer Science,
5499: Springer-Verlag, Berlin, Glasgow, UK, 1995.
5500:
5501: \bibitem{Schrijver99}
5502: A.~Schrijver, Theory of Linear and Integer Programming, Wiley Interscience
5503: Series in Discrete Mathematics and Optimization, John Wiley \& Sons, 1999.
5504:
5505: \bibitem{ShahamKS00}
5506: R.~Shaham, E.~K. Kolodner, S.~Sagiv, Automatic removal of array memory leaks in
5507: {J}ava, in: D.~A. Watt (ed.), Proceedings of the 9th International Conference
5508: on Compiler Construction (CC 2000), vol. 1781 of Lecture Notes in Computer
5509: Science, Springer-Verlag, Berlin, Berlin, Germany, 2000.
5510:
5511: \bibitem{SimonKH02}
5512: A.~Simon, A.~King, J.~M. Howe, Two variables per linear inequality as an
5513: abstract domain, in: M.~Leuschel (ed.), Logic Based Program Synthesis and
5514: Tranformation, 12th International Workshop, vol. 2664 of Lecture Notes in
5515: Computer Science, Springer-Verlag, Berlin, Madrid, Spain, 2002.
5516:
5517: \bibitem{SohnVG91}
5518: K.~Sohn, A.~{Van Gelder}, Termination detection in logic programs using
5519: argument sizes (extended abstract), in: Proceedings of the Tenth {ACM}
5520: {SIGACT-SIGMOD-SIGART} Symposium on Principles of Database Systems, ACM,
5521: Association for Computing Machinery, Denver, Colorado, United States, 1991.
5522:
5523: \bibitem{SongCR06}
5524: H.~Song, K.~J. Compton, W.~C. Rounds, {SPHIN:} a model checker for
5525: reconfigurable hybrid systems based on {SPIN}, in: R.~Lazic, R.~Nagarajan
5526: (eds.), Proceedings of the 5th International Workshop on Automated
5527: Verification of Critical Systems, vol. 145 of Electronic Notes in Theoretical
5528: Computer Science, University of Warwick, UK, 2006.
5529:
5530: \bibitem{StoerW70}
5531: J.~Stoer, C.~Witzgall, Convexity and Optimization in Finite Dimensions {I},
5532: Springer-Verlag, Berlin, 1970.
5533:
5534: \bibitem{vanHeeOSV06}
5535: K.~{van Hee}, O.~Oanea, N.~Sidorova, M.~Voorhoeve, Verifying generalized
5536: soundness for workflow nets, in: I.~Virbitskaite, A.~Voronkov (eds.),
5537: Perspectives of System Informatics: Proceedings of the Sixth International
5538: Andrei Ershov Memorial Conference, vol. 4378 of Lecture Notes in Computer
5539: Science, Springer-Verlag, Berlin, Akademgorodok, Novosibirsk, Russia, 2006.
5540:
5541: \bibitem{VenetB04}
5542: A.~Venet, G.~Brat, Precise and efficient static array bound checking for large
5543: embedded {C} programs, in: Proceedings of the ACM SIGPLAN 2004 Conference on
5544: Programming Language Design and Implementation (PLDI'04), ACM Press,
5545: Washington, DC, USA, 2004.
5546:
5547: \bibitem{Wilde93th}
5548: D.~K. Wilde, A library for doing polyhedral operations, {Master's thesis},
5549: Oregon State University, Corvallis, Oregon, also published as IRISA
5550: \emph{Publication interne} 785, Rennes, France, 1993 (Dec. 1993).
5551:
5552: \end{thebibliography}
5553:
5554: }%%\ifthenelse{\boolean{TR}}{%%
5555:
5556: \end{document}
5557: