Widening Operators for Weakly-Relational Numeric Abstractions (Extended Abstract)% \thanks{This work has been partly supported by projects ``Constraint Based Verification of Reactive Systems'' and ``AIDA --- Abstract Interpretation Design and Applications'' and by the Royal Society International Joint Project --- 2004/R1 Europe (ESEP). }
Roberto Bagnara\inst{1}
Patricia M. Hill\inst{2}
Elena Mazzi\inst{1}
Enea Zaffanella\inst{1}
cs0412043.tex
\documentclass[draft]{llncs}
 
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{url}
\usepackage{ifthen}

\newboolean{short}
%\setboolean{short}{true}
\setboolean{short}{false}

%% Summaries for theorem-like environments
\newcommand{\summary}[1]{\textrm{\textbf{\textup{#1}}}}

%% Special letters denoting sets and algebras
\providecommand*{\Nset}{\mathbb{N}}            % Naturals
\providecommand*{\Rset}{\mathbb{R}}            % Reals
\providecommand*{\nonnegRset}{\mathbb{R}_{\scriptscriptstyle{+}}}
                                               % Non-negative reals
\providecommand*{\CPset}{\mathbb{CP}}          % Closed polyhedra
\providecommand*{\Pset}{\mathbb{P}}            % (NNC) polyhedra

%% Calligraphic alphabet
\newcommand*{\cA}{\ensuremath{\mathcal{A}}}
\newcommand*{\cB}{\ensuremath{\mathcal{B}}}
\newcommand*{\cC}{\ensuremath{\mathcal{C}}}
\newcommand*{\cD}{\ensuremath{\mathcal{D}}}
\newcommand*{\cE}{\ensuremath{\mathcal{E}}}
\newcommand*{\cF}{\ensuremath{\mathcal{F}}}
\newcommand*{\cG}{\ensuremath{\mathcal{G}}}
\newcommand*{\cH}{\ensuremath{\mathcal{H}}}
\newcommand*{\cI}{\ensuremath{\mathcal{I}}}
\newcommand*{\cJ}{\ensuremath{\mathcal{J}}}
\newcommand*{\cK}{\ensuremath{\mathcal{K}}}
\newcommand*{\cL}{\ensuremath{\mathcal{L}}}
\newcommand*{\cM}{\ensuremath{\mathcal{M}}}
\newcommand*{\cN}{\ensuremath{\mathcal{N}}}
\newcommand*{\cO}{\ensuremath{\mathcal{O}}}
\newcommand*{\cP}{\ensuremath{\mathcal{P}}}
\newcommand*{\cQ}{\ensuremath{\mathcal{Q}}}
\newcommand*{\cR}{\ensuremath{\mathcal{R}}}
\newcommand*{\cS}{\ensuremath{\mathcal{S}}}
\newcommand*{\cT}{\ensuremath{\mathcal{T}}}
\newcommand*{\cU}{\ensuremath{\mathcal{U}}}
\newcommand*{\cV}{\ensuremath{\mathcal{V}}}
\newcommand*{\cW}{\ensuremath{\mathcal{W}}}
\newcommand*{\cX}{\ensuremath{\mathcal{X}}}
\newcommand*{\cY}{\ensuremath{\mathcal{Y}}}
\newcommand*{\cZ}{\ensuremath{\mathcal{Z}}}

%% Set theory

\renewcommand{\emptyset}{\mathord{\varnothing}}

%% \newcommand*{\wpc}{\mathop{\wp_\mathrm{c}}\nolimits}
\newcommand*{\wpf}{\mathop{\wp_\mathrm{f}}\nolimits}
\newcommand*{\wpfn}{\mathop{\wp_\mathrm{fn}}\nolimits}

% subset and supset relations
\newcommand*{\sseq}{\subseteq}
\newcommand*{\sseqf}{\mathrel{\subseteq_\mathrm{f}}}
\newcommand*{\sslt}{\subset}
\newcommand*{\Sseq}{\supseteq}
\newcommand*{\Ssgt}{\supset}
\newcommand{\Nsseq}{\nsubseteq}

% square subset and supset relations
\newcommand*{\sqsseq}{\sqsubseteq}
\newcommand*{\sqsslt}{\sqsubset}
\newcommand*{\sqSseq}{\sqsupseteq}
\newcommand*{\sqSsgt}{\sqsupset}
\newcommand{\Nsqsseq}{\not\sqsubseteq}

\newcommand*{\union}{\cup}
\newcommand*{\bigunion}{\bigcup}
\newcommand*{\biginters}{\bigcap}
\newcommand*{\inters}{\cap}
\newcommand*{\setdiff}{\setminus}

\newcommand{\sset}[2]{{\renewcommand{\arraystretch}{1.2}
                      \left\{\,#1 \,\left|\,
                               \begin{array}{@{}l@{}}#2\end{array}
                      \right.   \,\right\}}}

%% Declarators for functions and relations

\newcommand*{\monoarrow}{\mathrel{\buildrel\mathrm{m}\over\longrightarrow}}
\newcommand*{\contarrow}{\mathrel{\buildrel\mathrm{c}\over\longrightarrow}}

\newcommand*{\reld}[3]{\mathord{#1}\subseteq#2\times#3}
\newcommand*{\fund}[3]{\mathord{#1}\colon#2\rightarrow#3}
\newcommand*{\monofund}[3]{\mathord{#1}\colon#2\monoarrow#3}
\newcommand*{\contfund}[3]{\mathord{#1}\colon#2\contarrow#3}
\newcommand*{\pard}[3]{\mathord{#1}\colon#2\rightarrowtail#3}

%% Logical quantifiers stuff
\newcommand{\st}{\mathrel{.}}
\newcommand{\itc}{\mathrel{:}}

%% Lambda notation
\newcommand{\lambdadot}{\mathbin{.}}

% Matrix functions.
\newcommand*{\mat}{\mathop{\mathrm{matrix}}\nolimits}
\newcommand*{\transpose}{{\scriptscriptstyle\mathrm{T}}}

\spnewtheorem*{delayedproof}{Proof}{\bfseries}{\rmfamily}

% Relationship between two rays
\newcommand{\rrelation}{\mathrm{relation}}

% Generic upper-bound operator
\newcommand*{\ub}{\mathbin{\boxplus}}
% Generic widening
\newcommand*{\widen}{\mathbin{\nabla}}
% H79 widening
\newcommand*{\hwiden}{\mathbin{\nabla_s}}
% Improved but generic widening
\newcommand*{\gwiden}{\mathbin{\tilde{\nabla}}}
% BHRZ03 widening
%%\newcommand*{\bwiden}{\mathbin{\tilde{\nabla}_b}}
\newcommand*{\bwiden}{\mathbin{\hat{\nabla}}}

% BHRZ03 widening heuristics
\newcommand*{\Ht}{\mathop{h}\nolimits}

% Constraint and generator descriptions of polyhedra.
\newcommand*{\con}{\mathop{\mathrm{con}}\nolimits}
\newcommand*{\gen}{\mathop{\mathrm{gen}}\nolimits}

% Limited growth ordering relation.
\newcommand*{\lgo}{\mathrel{\curvearrowright}}
% Lexicographic limited growth ordering relation.
\newcommand*{\smallL}{{\scriptscriptstyle\mathrm{L}}}
\newcommand*{\lgoL}{\mathrel{\lgo_\smallL}}
% Powerset limited growth ordering relation.
\newcommand*{\smallP}{{\scriptscriptstyle\mathrm{P}}}
\newcommand*{\lgoP}{\mathrel{\lgo_\smallP}}
\newcommand*{\NlgoP}{\mathrel{{\not\lgo}_\smallP}}

% widening ordering relation.
\newcommand*{\ltwiden}{\mathrel{\sentailss{\widen}}}
\newcommand*{\leqwiden}{\mathrel{\entailss{\widen}}}

% Splitting equalities into pairs of inequalities.
\newcommand*{\geqrepr}{\mathop{\mathrm{repr}_{\mathord{\geq}}}\nolimits}

% Segments
\newcommand*{\opensegment}[2]{\left]{#1}, {#2}\right[}
\newcommand*{\closedsegment}[2]{\left[{#1}, {#2}\right]}

%% Logic notation
\newcommand*{\entails}{\mathrel{\vdash}}
\newcommand*{\bigland}{\mathop{\bigwedge}}
\newcommand*{\biglor}{\mathop{\bigvee}}
\newcommand*{\piff}{\mathrel{\leftrightarrow}}
\newcommand*{\pimplies}{\mathrel{\rightarrow}}
\newcommand*{\pimplied}{\mathrel{\leftarrow}}

%% Things that hold by definition
\newcommand{\defrel}[1]{\mathrel{\buildrel \mathrm{def} \over {#1}}}
%\newcommand{\defeq}{\defrel{=}}
\newcommand{\defeq}{\mathrel{\mathord{:}\mathord{=}}}
\newcommand{\defiff}{\defrel{\Longleftrightarrow}}
%\newcommand{\defeq}{=}
%\newcommand{\defiff}{\Longleftrightarrow}

%% Domain and co-domain of a function
\newcommand*{\dom}{\mathop{\mathrm{dom}}\nolimits}
\newcommand*{\cod}{\mathop{\mathrm{cod}}\nolimits}

%% Parameters of a substitution
\newcommand*{\param}{\mathop{\mathrm{param}}\nolimits}

%% Composition of functions
\newcommand*{\compose}{\mathbin{\circ}}

\newcommand*{\coanote}[1]{\footnote{\textbf{For co-authors:} {#1}}}
%\newcommand*{\coanote}[1]{}

\newcommand{\card}{\mathop{\#}\nolimits}
\newcommand{\cardnf}{\mathop{\#_{\mathrm{nf}}}\nolimits}
\newcommand*{\Min}{\inplus}

%% Cone generated by a set of rays
\newcommand*{\cone}{\mathop{\mathrm{cone}}\nolimits}

%% Dimension of a polyhedron
\newcommand*{\pdim}{\mathop{\mathrm{dim}}\nolimits}

%% The set of equality and inequality constraints in a constraint system.
\newcommand*{\eq}{\mathop{\mathrm{eq}}\nolimits}
\newcommand*{\ineq}{\mathop{\mathrm{ineq}}\nolimits}
%% The vector of the homogeneous coefficients of a constraint.
\newcommand*{\slope}{\mathop{\mathrm{slope}}\nolimits}

%% Orthogonal space.
\newcommand*{\orth}[1]{#1^\bot}
%% Affine hull.
\newcommand*{\affinehull}{\mathop{\mathrm{aff.hull}}\nolimits}
%% Characteristic cone
\newcommand*{\charcone}{\mathop{\mathrm{char.cone}}\nolimits}
%% Lineality space
\newcommand*{\linspace}{\mathop{\mathrm{lin.space}}\nolimits}
%% Ray space
\newcommand*{\rayspace}{\mathop{\mathrm{ray.space}}\nolimits}
%% Topological closure
\newcommand*{\topclosure}{\mathop{\mathbb{C}}\nolimits}
%% Binary convex polyhedral hull.
\newcommand*{\polyhull}{\uplus}
%% Polyhedral hull (for a set of polyhedra).
\newcommand*{\bigpolyhull}{\mathop{\biguplus}\nolimits}
%% Polyhedral difference.
\newcommand*{\polydiff}{\mathop{\mathrm{diff}}\nolimits}

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

%% Assignment

\newcommand*{\takes}{\mathrel{:=}}

%% Definition
\newtheorem{Def}{Definition}

%% Uncomment this for page numbers.
\pagestyle{plain}

\begin{document}
\ifthenelse{\boolean{short}}
{%
\title{Widening Operators for Weakly-Relational Numeric Abstractions
       (Extended Abstract)%
\thanks{This work has been partly supported by projects
  ``Constraint Based Verification of Reactive Systems''
  and
  ``AIDA --- Abstract Interpretation Design and Applications''
  and
  by the Royal Society International Joint Project --- 2004/R1 Europe (ESEP).
}
}
}{%
\title{Widening Operators \\ for Weakly-Relational Numeric Abstractions%
\thanks{This work has been partly supported by projects
  ``Constraint Based Verification of Reactive Systems''
  and
  ``AIDA --- Abstract Interpretation Design and Applications''
  and
  by the Royal Society International Joint Project --- 2004/R1 Europe (ESEP).
}
}
\subtitle{(Extended Abstract)}
}
\author{Roberto Bagnara\inst{1}
\and Patricia M. Hill\inst{2}
\and Elena Mazzi\inst{1}
\and Enea Zaffanella\inst{1}
}
\authorrunning{R.~Bagnara,
               P.~M.~Hill,
               E.~Mazzi,
               E.~Zaffanella,
}
\tocauthor{Roberto Bagnara (University of Parma),
           Patricia M. Hill (University of Leeds),
           Elena Mazzi (University of Parma),
           Enea Zaffanella (University of Parma)
}

\institute{
    Department of Mathematics,
    University of Parma,
    Italy \\
    \email{\{bagnara,%
             mazzi,%
             zaffanella\}@cs.unipr.it}
\and
    School of Computing,
    University of Leeds,
    UK \\
    \email{hill@comp.leeds.ac.uk}
}
                                                                                
\maketitle

\ifthenelse{\boolean{short}}
{%
\enlargethispage{4mm}
}{%
\section{Introduction}
}
In recent years there has been a lot of interest in the definition of
so-called \emph{weakly-relational} numeric domains, whose complexity
and precision are in between the (non-relational) abstract domain of
intervals~\cite{CousotC77} and the (relational) abstract domain of
convex polyhedra~\cite{CousotH78}.
%
The first weakly-relational domain proposed in the literature is based
on systems of constraints of the form $x - y \leq c$ and $\pm x \leq c$,
typically represented by Difference-Bound Matrices (DBMs).  Even
though DBMs have a long tradition in Computer Science, their use in
the Abstract Interpretation field is quite recent. The idea of
defining an abstract domain of DBMs was put forward
in~\cite{Bagnara97th}, where these constraints were called
\emph{bounded differences}.  An independent application can be found
in~\cite{ShahamKS00}, where an abstract domain of transitively closed
DBMs is defined.  In this case, the transitive closure requirement was
meant as a simple and well understood way to obtain a
\emph{canonical form} for the domain elements, so as to abstract away
from merely syntactic differences.  In~\cite{ShahamKS00}
the specification of all the required abstract semantics operators
is provided, including an operator that is meant to match
the \emph{standard widening} operator defined on the domain of convex
polyhedra~\cite{CousotH78}.
Unfortunately, as pointed out in~\cite{Mine01a,Mine01b}, this operator
is not a widening since it does not provide a convergence guarantee
for the abstract iteration sequence.

The abstract domain of (not necessarily transitively closed) DBMs is
considered in~\cite{Mine01a}.  In this more concrete, syntactic domain
the transitive closure operator behaves as a kernel operator
(monotonic, idempotent and reductive) mapping each DBM into the
smallest DBM (with respect to the component-wise ordering)
encoding the same geometric shape.
As done in~\cite{ShahamKS00}, a widening operator is
also defined in~\cite{Mine01a} and it is observed that this widening
``has some intriguing interactions'' with transitive closure,
therefore identifying the divergence issue faced in~\cite{ShahamKS00}.
This observation has led to the conclusion that
``fixpoint computations \emph{must} be performed''
in the lattice of DBMs, without enforcing transitive closure \cite{Mine01a}.

\section{Difference-Bound Shapes}

While the analysis of the divergence problem is absolutely correct,
the solution identified in~\cite{Mine01a} is sub-optimal
since, as is usually the case, resorting to a syntactic domain
(such as the one of DBMs) has a number of negative consequences.
%
To identify a simpler, more natural solution, we first have to
acknowledge that an element of this abstract domain should be a
geometric shape, rather than (any) one of its matrix
representations. To stress this concept, such an element will be
called a \emph{Difference-Bound Shape} (DBS).  A DBS corresponds to
the equivalence class of all the DBMs representing it.  The
implementation of the abstract domain can freely choose between these
possible representations, switching at will from one to the other, as
long as the semantic operators are implemented as expected.
%
The other step towards the solution of the divergence problem is the
simple observation that a DBS is a convex polyhedron and the set of
all DBSs is closed under the application of the standard widening on
polyhedra. Thus, no divergence problem can be incurred when applying
the standard widening to an increasing sequence of DBSs.

On the other hand, the domain of DBSs is isomorphic to the domain of
transitively closed DBMs considered in~\cite{ShahamKS00}, which
suffers from an actual divergence problem.  A closer inspection
reveals that these two observations are not in contradiction, because
the widening operator defined in~\cite{ShahamKS00} is not
equivalent to the standard widening for convex polyhedra.
%
In fact, a key requirement in the specification of the standard
widening is that the first argument is described by a non-redundant
system of
\ifthenelse{\boolean{short}}
{%
constraints.
}{%
constraints.\footnote{This requirement was sometimes neglected in recent
papers describing the standard widening; it was recently recalled and
exemplified in~\cite{BagnaraHRZ03,BagnaraHRZ05SCP}.}
}
Thus, using transitively closed DBMs does not work because they
typically contain redundant constraints.
What is needed for a correct implementation of the standard widening
is a minimization procedure mapping a DBM representation into (any)
one of the maximal elements in the corresponding equivalence class:
such a procedure was defined in~\cite{LarsenLPY97} and called
\emph{transitive reduction}.

In summary, the solution to the divergence problem for DBSs is to
apply the standard widening of~\cite{CousotH78} to a transitively reduced DBM
representation of the first argument. It is worth stressing that, from
the point of view of the user, this is a transparent implementation
detail: on the domain of DBSs, transitive reduction is the identity
function, as was the case for transitive closure.

\subsection{On the Precision of the Standard Widening}

The standard widening on DBSs
%, though well-defined,\footnote{By assuming a fixed order on variables,
%the transitive reduction algorithm provides another canonical form
%representation for DBSs.}
could result, if used without any precaution, in poorer precision
with respect to its counterpart defined on the syntactic domain of DBMs.
%
The specification of~\cite{Mine01a} prescribes, for maximum precision,
two constraints on the abstract iteration sequence:
the first one restricts the application of the standard widening to a
transitively closed representation for the second argument (note that,
in this case, no divergence problem can arise);
the second one demands that the first DBM of the iteration sequence
$M_0$, $M_1$, \dots,~$M_i$, \dots is transitively closed.
%
The effects of both improvements can be obtained also with the
semantic domain of DBSs. As for the first one, this can be applied
as is (since transitive closure is just an implementation detail).
The other improvement can be achieved by applying the
well-known `widening up to' technique defined
in~\cite{HalbwachsPR94,HalbwachsPR97}
or its variation called `staged widening with thresholds'
\cite{BlanchetCCFMMMR02,BlanchetCCFMMMR03,Mine04}:
in practice, it is sufficient to add to the set of `up to' thresholds
all the constraints of $M_0$ that are redundant for the representation
of the corresponding DBS (i.e., those constraints that are removed by
the transitive reduction algorithm).

Further precision improvements can be obtained by applying any delay
strategy and/or the framework defined
in~\cite{BagnaraHRZ03,BagnaraHRZ05SCP}.  In particular, by providing
the widening on DBSs with a finite convergence certificate, it is
possible to lift it to a corresponding widening on the \emph{finite powerset}
of DBSs~\cite{BagnaraHZ03b}. It should be stressed that, in this case,
using the syntactic domain of DBMs may have drawbacks: since different
DBMs may represent the same DBS, the presence of these ``duplicates''
in a finite powerset element may have a negative effect on both
efficiency and precision (e.g., when considering a \emph{cardinality-based}
widening operator).  Also note that, in general, the systematic
removal of these duplicates would interfere with widenings, possibly
compromising the convergence guarantee.

\section{Octagonal Shapes and Beyond}

The abstract domain of DBMs has been generalized in~\cite{Mine01b} so
as to allow for the manipulation of constraints of the form
$a x + b y \leq c$, where $a,b \in \{-1,0,+1\}$, leading to the
definition of the \emph{octagon} abstract
\ifthenelse{\boolean{short}}
{%
domain.
}{%
(octagons were called \emph{simple sections} in~\cite{BalasundaramK89}).
}
Each octagon is represented by using a \emph{coherent} DBM
and the transitive closure algorithm is specialized into a
\emph{strong closure} procedure. All the previous reasoning can be
repeated, leading to the definition of the semantic abstract domain of
\emph{octagonal shapes} together with a correct implementation of the
standard widening. In this case, the transitive reduction
algorithm defined in~\cite{LarsenLPY97} does not eliminate all
redundancies: we will describe a new minimization procedure that takes
into account all the constraint inferences performed by the strong
closure algorithm.

Other examples of weakly-relational numeric domains include the `two
variables per inequality' abstract domain~\cite{SimonKH02}, the
octahedron abstract domain~\cite{ClarisoC04}, and the abstract domain
of template constraint matrices~\cite{SankaranarayananSM05}, as well
as the abstract domain of bounded quotients~\cite{Bagnara97th} and the
zone congruence abstract domain \cite{Mine02}.  As long as their
implementation is based on (extensions of) the transitive closure
algorithm, it is possible to define the corresponding syntactic and
semantic versions. The choice between the two versions mainly depends
on the availability of a reasonably efficient minimization procedure:
in our opinion, all the rest being equal, the semantic versions should
be preferred for their greater elegance and the more natural
integration with domain constructions such as the finite powerset
operator.

\ifthenelse{\boolean{short}}
{%
\newcommand{\noopsort}[1]{}\hyphenation{ Ba-gna-ra Bie-li-ko-va Bruy-noo-ghe
  Common-Loops DeMich-iel Dober-kat Di-par-ti-men-to Er-vier Fa-la-schi
  Fell-eisen Gam-ma Gem-Stone Glan-ville Gold-in Goos-sens Graph-Trace
  Grim-shaw Her-men-e-gil-do Hoeks-ma Hor-o-witz Kam-i-ko Kenn-e-dy Kess-ler
  Lisp-edit Lu-ba-chev-sky Ma-te-ma-ti-ca Nich-o-las Obern-dorf Ohsen-doth
  Par-log Para-sight Pega-Sys Pren-tice Pu-ru-sho-tha-man Ra-guid-eau Rich-ard
  Roe-ver Ros-en-krantz Ru-dolph SIG-OA SIG-PLAN SIG-SOFT SMALL-TALK Schee-vel
  Schlotz-hauer Schwartz-bach Sieg-fried Small-talk Spring-er Stroh-meier
  Thing-Lab Zhong-xiu Zac-ca-gni-ni Zaf-fa-nel-la Zo-lo }
\begin{thebibliography}{10}

\bibitem{Bagnara97th}
R.~Bagnara.
\newblock {\em Data-Flow Analysis for Constraint Logic-Based Languages}.
\newblock PhD thesis, Dipartimento di Informatica, Universit\`a di Pisa, Pisa,
  Italy, March 1997.

\bibitem{BagnaraHRZ03}
R.~Bagnara, P.~M. Hill, E.~Ricci, and E.~Zaffanella.
\newblock Precise widening operators for convex polyhedra.
\newblock In R.~Cousot, editor, {\em Proceedings of SAS'03}, volume 2694 of LNCS, pages 337--354, San Diego, California, USA, 2003. Springer-Verlag.

\bibitem{BagnaraHRZ05SCP}
R.~Bagnara, P.~M. Hill, E.~Ricci, and E.~Zaffanella.
\newblock Precise widening operators for convex polyhedra.
\newblock {\em Science of Computer Programming}, 2005.
\newblock To appear.

\bibitem{BagnaraHZ03b}
R.~Bagnara, P.~M. Hill, and E.~Zaffanella.
\newblock Widening operators for powerset domains.
\newblock In B.~Steffen and G.~Levi, editors, {\em Proceedings of VMCAI'04}, volume 2937 of LNCS, pages 135--148, Venice, Italy, 2003. Springer-Verlag.

\bibitem{BlanchetCCFMMMR02}
B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
  D.~Monniaux, and X.~Rival.
\newblock Design and implementation of a special-purpose static program
  analyzer for safety-critical real-time embedded software.
\newblock In T.~{\AE}. Mogensen, D.~A. Schmidt, and I.~Hal Sudborough, editors,
  {\em The Essence of Computation}, volume 2566 of LNCS, pages 85--108. Springer-Verlag, 2002.

\bibitem{BlanchetCCFMMMR03}
B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
  D.~Monniaux, and X.~Rival.
\newblock A static analyzer for large safety-critical software.
\newblock In {\em Proceedings of PLDI'03}, pages 196--207, San Diego,
  California, USA, 2003. ACM Press.

\bibitem{ClarisoC04}
R.~Claris\'{o} and J.~Cortadella.
\newblock The octahedron abstract domain.
\newblock In R.~Giacobazzi, editor, {\em Proceedings of SAS'04}, volume 3148 of LNCS, pages 312--327, Verona, Italy, 2004. Springer-Verlag.

\bibitem{CousotC77}
P.~Cousot and R.~Cousot.
\newblock Abstract interpretation: {A} unified lattice model for static
  analysis of programs by construction or approximation of fixpoints.
\newblock In {\em Proceedings of POPL'77}, pages 238--252, New York, 1977. ACM Press.

\bibitem{CousotH78}
P.~Cousot and N.~Halbwachs.
\newblock Automatic discovery of linear restraints among variables of a
  program.
\newblock In {\em Proceedings of POPL'78}, pages 84--96, Tucson, Arizona, 1978.
  ACM Press.

\bibitem{HalbwachsPR94}
N.~Halbwachs, Y.-E. Proy, and P.~Raymond.
\newblock Verification of linear hybrid systems by means of convex
  approximations.
\newblock In B.~{Le Charlier}, editor, {\em Proceedings of SAS'94}, volume 864 of LNCS, pages 223--237, Namur, Belgium, 1994. Springer-Verlag.

\bibitem{HalbwachsPR97}
N.~Halbwachs, Y.-E. Proy, and P.~Roumanoff.
\newblock Verification of real-time systems using linear relation analysis.
\newblock {\em Formal Methods in System Design}, 11(2):157--185, 1997.

\bibitem{LarsenLPY97}
K.~Larsen, F.~Larsson, P.~Pettersson, and W.~Yi.
\newblock Efficient verification of real-time systems: Compact data structure
  and state-space reduction.
\newblock In {\em Proceedings of RTSS'97}, pages 14--24, San Francisco, CA, 1997. IEEE Computer Society
  Press.

\bibitem{Mine01a}
A.~Min\'e.
\newblock A new numerical abstract domain based on difference-bound matrices.
\newblock In {\em Proceedings of PADO'01}, volume 2053 of LNCS, pages
  155--172, Aarhus, Denmark, 2001. Springer-Verlag.

\bibitem{Mine01b}
A.~Min\'e.
\newblock The octagon abstract domain.
\newblock In {\em Proceedings of WCRE'01}, pages 310--319, Stuttgart, Germany, 2001. IEEE
  Computer Society Press.

\bibitem{Mine02}
A.~Min\'e.
\newblock A few graph-based relational numerical abstract domains.
\newblock In M.~V. Hermenegildo and G.~Puebla, editors,
 {\em Proceedings of SAS'02}, volume 2477 of LNCS, pages 117--132, Madrid, Spain, 2002. Springer-Verlag.

\bibitem{Mine04}
A.~Min\'e.
\newblock Relational abstract domains for the detection of floating-point
  run-time errors.
\newblock In D.~Schmidt, editor, {\em Proceedings ESOP'04}, volume 2986 of LNCS, pages 3--17, Barcelona, Spain, 2004. Springer-Verlag.

\bibitem{SankaranarayananSM05}
S.~Sankaranarayanan, H.~Sipma, and Z.~Manna.
\newblock Scalable analysis of linear systems using mathematical programming.
\newblock In R.~Cousot, editor, {\em Proceedings of VMCAI'05}, volume 3385 of LNCS, Paris,
  France, 2004. Springer-Verlag.
\newblock To appear.

\bibitem{ShahamKS00}
R.~Shaham, E.~K. Kolodner, and S.~Sagiv.
\newblock Automatic removal of array memory leaks in {J}ava.
\newblock In D.~A. Watt, editor, {\em Proceedings of CC'00}, volume 1781 of LNCS, pages 50--66. Springer-Verlag, 2000.

\bibitem{SimonKH02}
A.~Simon, A.~King, and J.~M. Howe.
\newblock Two variables per linear inequality as an abstract domain.
\newblock In M.~Leuschel, editor, {\em Proceedings of LOPSTR'02}, volume 2664 of LNCS,
  pages 71--89, Madrid, Spain, 2002.
  Springer-Verlag.
\end{thebibliography}
}{%
%%\bibliographystyle{plain}
%%\bibliography{ppl,mybib}
\newcommand{\noopsort}[1]{}\hyphenation{ Ba-gna-ra Bie-li-ko-va Bruy-noo-ghe
  Common-Loops DeMich-iel Dober-kat Di-par-ti-men-to Er-vier Fa-la-schi
  Fell-eisen Gam-ma Gem-Stone Glan-ville Gold-in Goos-sens Graph-Trace
  Grim-shaw Her-men-e-gil-do Hoeks-ma Hor-o-witz Kam-i-ko Kenn-e-dy Kess-ler
  Lisp-edit Lu-ba-chev-sky Ma-te-ma-ti-ca Nich-o-las Obern-dorf Ohsen-doth
  Par-log Para-sight Pega-Sys Pren-tice Pu-ru-sho-tha-man Ra-guid-eau Rich-ard
  Roe-ver Ros-en-krantz Ru-dolph SIG-OA SIG-PLAN SIG-SOFT SMALL-TALK Schee-vel
  Schlotz-hauer Schwartz-bach Sieg-fried Small-talk Spring-er Stroh-meier
  Thing-Lab Zhong-xiu Zac-ca-gni-ni Zaf-fa-nel-la Zo-lo }
\begin{thebibliography}{10}

\bibitem{Bagnara97th}
R.~Bagnara.
\newblock {\em Data-Flow Analysis for Constraint Logic-Based Languages}.
\newblock PhD thesis, Dipartimento di Informatica, Universit\`a di Pisa, Pisa,
  Italy, March 1997.
\newblock Printed as Report TD-1/97.

\bibitem{BagnaraHRZ03}
R.~Bagnara, P.~M. Hill, E.~Ricci, and E.~Zaffanella.
\newblock Precise widening operators for convex polyhedra.
\newblock In R.~Cousot, editor, {\em Static Analysis: Proceedings of the 10th
  International Symposium}, volume 2694 of {\em Lecture Notes in Computer
  Science}, pages 337--354, San Diego, California, USA, 2003. Springer-Verlag,
  Berlin.

\bibitem{BagnaraHRZ05SCP}
R.~Bagnara, P.~M. Hill, E.~Ricci, and E.~Zaffanella.
\newblock Precise widening operators for convex polyhedra.
\newblock {\em Science of Computer Programming}, 2005.
\newblock To appear.

\bibitem{BagnaraHZ03b}
R.~Bagnara, P.~M. Hill, and E.~Zaffanella.
\newblock Widening operators for powerset domains.
\newblock In B.~Steffen and G.~Levi, editors, {\em Proceedings of the Fifth
  International Conference on Verification, Model Checking and Abstract
  Interpretation (VMCAI 2004)}, volume 2937 of {\em Lecture Notes in Computer
  Science}, pages 135--148, Venice, Italy, 2003. Springer-Verlag, Berlin.

\bibitem{BalasundaramK89}
V.~Balasundaram and K.~Kennedy.
\newblock A technique for summarizing data access and its use in parallelism
  enhancing transformations.
\newblock In B.~Knobe, editor, {\em Proceedings of the ACM SIGPLAN'89
  Conference on Programming Language Design and Implementation (PLDI)}, volume
  24(7) of {\em ACM SIGPLAN Notices}, pages 41--53, Portland, Oregon, USA,
  1989. ACM Press.

\bibitem{BlanchetCCFMMMR02}
B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
  D.~Monniaux, and X.~Rival.
\newblock Design and implementation of a special-purpose static program
  analyzer for safety-critical real-time embedded software.
\newblock In T.~{\AE}. Mogensen, D.~A. Schmidt, and I.~Hal Sudborough, editors,
  {\em The Essence of Computation}, volume 2566 of {\em Lecture Notes in
  Computer Science}, pages 85--108. Springer-Verlag, Berlin, 2002.

\bibitem{BlanchetCCFMMMR03}
B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
  D.~Monniaux, and X.~Rival.
\newblock A static analyzer for large safety-critical software.
\newblock In {\em Proceedings of the ACM SIGPLAN 2003 Conference on Programming
  Language Design and Implementation (PLDI'03)}, pages 196--207, San Diego,
  California, USA, 2003. ACM Press.

\bibitem{ClarisoC04}
R.~Claris\'{o} and J.~Cortadella.
\newblock The octahedron abstract domain.
\newblock In R.~Giacobazzi, editor, {\em Static Analysis: Proceedings of the
  11th International Symposium}, volume 3148 of {\em Lecture Notes in Computer
  Science}, pages 312--327, Verona, Italy, 2004. Springer-Verlag, Berlin.

\bibitem{CousotC77}
P.~Cousot and R.~Cousot.
\newblock Abstract interpretation: {A} unified lattice model for static
  analysis of programs by construction or approximation of fixpoints.
\newblock In {\em Proceedings of the Fourth Annual ACM Symposium on Principles
  of Programming Languages}, pages 238--252, New York, 1977. ACM Press.

\bibitem{CousotH78}
P.~Cousot and N.~Halbwachs.
\newblock Automatic discovery of linear restraints among variables of a
  program.
\newblock In {\em Conference Record of the Fifth Annual ACM Symposium on
  Principles of Programming Languages}, pages 84--96, Tucson, Arizona, 1978.
  ACM Press.

\bibitem{HalbwachsPR94}
N.~Halbwachs, Y.-E. Proy, and P.~Raymond.
\newblock Verification of linear hybrid systems by means of convex
  approximations.
\newblock In B.~{Le Charlier}, editor, {\em Static Analysis: Proceedings of the
  1st International Symposium}, volume 864 of {\em Lecture Notes in Computer
  Science}, pages 223--237, Namur, Belgium, 1994. Springer-Verlag, Berlin.

\bibitem{HalbwachsPR97}
N.~Halbwachs, Y.-E. Proy, and P.~Roumanoff.
\newblock Verification of real-time systems using linear relation analysis.
\newblock {\em Formal Methods in System Design}, 11(2):157--185, 1997.

\bibitem{LarsenLPY97}
K.~Larsen, F.~Larsson, P.~Pettersson, and W.~Yi.
\newblock Efficient verification of real-time systems: Compact data structure
  and state-space reduction.
\newblock In {\em Proceedings of the 18th IEEE Real-Time Systems Symposium
  (RTSS'97)}, pages 14--24, San Francisco, CA, 1997. IEEE Computer Society
  Press.

\bibitem{Mine01a}
A.~Min\'e.
\newblock A new numerical abstract domain based on difference-bound matrices.
\newblock In O.~Danvy and A.~Filinski, editors, {\em Proceedings of the 2nd
  Symposium on Programs as Data Objects (PADO 2001)}, volume 2053 of {\em
  Lecture Notes in Computer Science}, pages 155--172, Aarhus, Denmark, 2001.
  Springer-Verlag, Berlin.

\bibitem{Mine01b}
A.~Min\'e.
\newblock The octagon abstract domain.
\newblock In {\em Proceedings of the Eighth Working Conference on Reverse
  Engineering (WCRE'01)}, pages 310--319, Stuttgart, Germany, 2001. IEEE
  Computer Society Press.

\bibitem{Mine02}
A.~Min\'e.
\newblock A few graph-based relational numerical abstract domains.
\newblock In M.~V. Hermenegildo and G.~Puebla, editors, {\em Static Analysis:
  Proceedings of the 9th International Symposium}, volume 2477 of {\em Lecture
  Notes in Computer Science}, pages 117--132, Madrid, Spain, 2002.
  Springer-Verlag, Berlin.

\bibitem{Mine04}
A.~Min\'e.
\newblock Relational abstract domains for the detection of floating-point
  run-time errors.
\newblock In D.~Schmidt, editor, {\em Programming Languages and Systema:
  Proceedings of the 13th European Symposium on Programming}, volume 2986 of
  {\em Lecture Notes in Computer Science}, pages 3--17, Barcelona, Spain, 2004.
  Springer-Verlag, Berlin.

\bibitem{SankaranarayananSM05}
S.~Sankaranarayanan, H.~Sipma, and Z.~Manna.
\newblock Scalable analysis of linear systems using mathematical programming.
\newblock In R.~Cousot, editor, {\em Proceedings of the Sixth International
  Conference on Verification, Model Checking and Abstract Interpretation (VMCAI
  2005)}, volume 3385 of {\em Lecture Notes in Computer Science}, Paris,
  France, 2004. Springer-Verlag, Berlin.
\newblock To appear.

\bibitem{ShahamKS00}
R.~Shaham, E.~K. Kolodner, and S.~Sagiv.
\newblock Automatic removal of array memory leaks in {J}ava.
\newblock In D.~A. Watt, editor, {\em Proceedings of the 9th International
  Conference on Compiler Construction (CC 2000)}, volume 1781 of {\em Lecture
  Notes in Computer Science}, pages 50--66. Springer-Verlag, Berlin, 2000.

\bibitem{SimonKH02}
A.~Simon, A.~King, and J.~M. Howe.
\newblock Two variables per linear inequality as an abstract domain.
\newblock In M.~Leuschel, editor, {\em Logic Based Program Synthesis and
  Tranformation, 12th International Workshop}, volume 2664 of {\em Lecture
  Notes in Computer Science}, pages 71--89, Madrid, Spain, 2002.
  Springer-Verlag, Berlin.

\end{thebibliography}
}

\end{document}

cs0412043.extracted_bib
\begin{thebibliography}{10}

\bibitem{Bagnara97th}
R.~Bagnara.
\newblock {\em Data-Flow Analysis for Constraint Logic-Based Languages}.
\newblock PhD thesis, Dipartimento di Informatica, Universit\`a di Pisa, Pisa,
  Italy, March 1997.

\bibitem{BagnaraHRZ03}
R.~Bagnara, P.~M. Hill, E.~Ricci, and E.~Zaffanella.
\newblock Precise widening operators for convex polyhedra.
\newblock In R.~Cousot, editor, {\em Proceedings of SAS'03}, volume 2694 of LNCS, pages 337--354, San Diego, California, USA, 2003. Springer-Verlag.

\bibitem{BagnaraHRZ05SCP}
R.~Bagnara, P.~M. Hill, E.~Ricci, and E.~Zaffanella.
\newblock Precise widening operators for convex polyhedra.
\newblock {\em Science of Computer Programming}, 2005.
\newblock To appear.

\bibitem{BagnaraHZ03b}
R.~Bagnara, P.~M. Hill, and E.~Zaffanella.
\newblock Widening operators for powerset domains.
\newblock In B.~Steffen and G.~Levi, editors, {\em Proceedings of VMCAI'04}, volume 2937 of LNCS, pages 135--148, Venice, Italy, 2003. Springer-Verlag.

\bibitem{BlanchetCCFMMMR02}
B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
  D.~Monniaux, and X.~Rival.
\newblock Design and implementation of a special-purpose static program
  analyzer for safety-critical real-time embedded software.
\newblock In T.~{\AE}. Mogensen, D.~A. Schmidt, and I.~Hal Sudborough, editors,
  {\em The Essence of Computation}, volume 2566 of LNCS, pages 85--108. Springer-Verlag, 2002.

\bibitem{BlanchetCCFMMMR03}
B.~Blanchet, P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e,
  D.~Monniaux, and X.~Rival.
\newblock A static analyzer for large safety-critical software.
\newblock In {\em Proceedings of PLDI'03}, pages 196--207, San Diego,
  California, USA, 2003. ACM Press.

\bibitem{ClarisoC04}
R.~Claris\'{o} and J.~Cortadella.
\newblock The octahedron abstract domain.
\newblock In R.~Giacobazzi, editor, {\em Proceedings of SAS'04}, volume 3148 of LNCS, pages 312--327, Verona, Italy, 2004. Springer-Verlag.

\bibitem{CousotC77}
P.~Cousot and R.~Cousot.
\newblock Abstract interpretation: {A} unified lattice model for static
  analysis of programs by construction or approximation of fixpoints.
\newblock In {\em Proceedings of POPL'77}, pages 238--252, New York, 1977. ACM Press.

\bibitem{CousotH78}
P.~Cousot and N.~Halbwachs.
\newblock Automatic discovery of linear restraints among variables of a
  program.
\newblock In {\em Proceedings of POPL'78}, pages 84--96, Tucson, Arizona, 1978.
  ACM Press.

\bibitem{HalbwachsPR94}
N.~Halbwachs, Y.-E. Proy, and P.~Raymond.
\newblock Verification of linear hybrid systems by means of convex
  approximations.
\newblock In B.~{Le Charlier}, editor, {\em Proceedings of SAS'94}, volume 864 of LNCS, pages 223--237, Namur, Belgium, 1994. Springer-Verlag.

\bibitem{HalbwachsPR97}
N.~Halbwachs, Y.-E. Proy, and P.~Roumanoff.
\newblock Verification of real-time systems using linear relation analysis.
\newblock {\em Formal Methods in System Design}, 11(2):157--185, 1997.

\bibitem{LarsenLPY97}
K.~Larsen, F.~Larsson, P.~Pettersson, and W.~Yi.
\newblock Efficient verification of real-time systems: Compact data structure
  and state-space reduction.
\newblock In {\em Proceedings of RTSS'97}, pages 14--24, San Francisco, CA, 1997. IEEE Computer Society
  Press.

\bibitem{Mine01a}
A.~Min\'e.
\newblock A new numerical abstract domain based on difference-bound matrices.
\newblock In {\em Proceedings of PADO'01}, volume 2053 of LNCS, pages
  155--172, Aarhus, Denmark, 2001. Springer-Verlag.

\bibitem{Mine01b}
A.~Min\'e.
\newblock The octagon abstract domain.
\newblock In {\em Proceedings of WCRE'01}, pages 310--319, Stuttgart, Germany, 2001. IEEE
  Computer Society Press.

\bibitem{Mine02}
A.~Min\'e.
\newblock A few graph-based relational numerical abstract domains.
\newblock In M.~V. Hermenegildo and G.~Puebla, editors,
 {\em Proceedings of SAS'02}, volume 2477 of LNCS, pages 117--132, Madrid, Spain, 2002. Springer-Verlag.

\bibitem{Mine04}
A.~Min\'e.
\newblock Relational abstract domains for the detection of floating-point
  run-time errors.
\newblock In D.~Schmidt, editor, {\em Proceedings ESOP'04}, volume 2986 of LNCS, pages 3--17, Barcelona, Spain, 2004. Springer-Verlag.

\bibitem{SankaranarayananSM05}
S.~Sankaranarayanan, H.~Sipma, and Z.~Manna.
\newblock Scalable analysis of linear systems using mathematical programming.
\newblock In R.~Cousot, editor, {\em Proceedings of VMCAI'05}, volume 3385 of LNCS, Paris,
  France, 2004. Springer-Verlag.
\newblock To appear.

\bibitem{ShahamKS00}
R.~Shaham, E.~K. Kolodner, and S.~Sagiv.
\newblock Automatic removal of array memory leaks in {J}ava.
\newblock In D.~A. Watt, editor, {\em Proceedings of CC'00}, volume 1781 of LNCS, pages 50--66. Springer-Verlag, 2000.

\bibitem{SimonKH02}
A.~Simon, A.~King, and J.~M. Howe.
\newblock Two variables per linear inequality as an abstract domain.
\newblock In M.~Leuschel, editor, {\em Proceedings of LOPSTR'02}, volume 2664 of LNCS,
  pages 71--89, Madrid, Spain, 2002.
  Springer-Verlag.
\end{thebibliography}