Abstract Interpretation
Web page maintained by P. Cousot
Last update: Aug 5, 2008
Contents
1 Introduction to Abstract Interpretation
2 What can be formalized by abstract interpretation?
2.1 Syntax
2.2 Semantics
2.3 Proofs
2.4 Static analysis
2.5 Dataflow Analysis
2.6 Controlflow Analysis
2.7 Types
2.8 Modelchecking
2.9 Predicate abstraction
2.10 Counterexamplebased refinement
2.11 Strong Preservation
2.12 Program transformation
2.13 Watermarking
2.14 Information hiding
2.15 Code obfuscation
2.16 Malware detection
2.17 Termination
3 Topics in abstract interpretation
3.1 Abstract domains
3.2 Finite versus infinite abstract domains
3.3 Merge over all paths (MOP) in dataflow analysis
3.4 Standard and collecting semantics
3.5 Galois connection
3.6 Moore family, Closure operators
3.7 Moore completion
3.8 Fixpoints
3.9 Inference rules
3.10 Iteration
3.11 Convergence acceleration by widening/narrowing
3.12 Constraint resolution
3.13 Modularity
3.14 Abstract domain combination
3.15 Refinement
3.16 Completion
3.17 Lattice of abstract interpretations
4 Examples of abstractinterpretationbased static analyses
4.1 Numerical Analysis
4.2 Interval analysis
4.3 Octagonal analysis
4.4 Polyhedral analysis
4.5 Congruence analysis
4.6 Roundoff error analysis
4.7 Symbolic analysis
4.8 Strictness and comportment analysis
4.9 Control flow analysis (CFA)
4.10 Escape analysis
4.11 Mode inference/groundness/sharing analysis
4.12 Aliasing and pointer analysis
4.13 Heap analysis
4.14 Concurrency analysis
4.15 Mobility analysis
4.16 Probabilistic analysis
4.17 WCET analysis
4.18 Hardware analysis
5 Libraries of abstract domains
5.1 The NewPolka polyhedral library
5.2 The Parma Polyhedra Library (PPL)
5.3 The octagon abstract domain library
6 Abstractinterpretationbased tools
6.1 Airac5
6.2 aiT WCET Analyzers
6.3 ASTRÉE
6.4 C Global Surveyor
6.5 Fluctuat
6.6 PolySpace Verifier
6.7 TERMINATOR
6.8 TVLA
7 Main conferences in abstract interpretation
8 Short bibliography
1 Introduction to Abstract Interpretation
The formal verification of a program (and more generally a
computer system) consists in proving that its semantics
(describing "what the program executions actually do") satisfies its
specification (describing "what the program executions are
supposed to do").
Abstract interpretation
[22,26] formalizes the idea
that this formal proof can be done at some level of abstraction where
irrelevant details about the semantics and the specification are
ignored. This amounts to proving that an abstract semantics
satisfies an abstract specification. An example of abstract
semantics is Hoare logic while examples of abstract specifications are
invariance, partial, or total correctness. This abstracts away from
concrete properties such as execution times.
Abstractions should preferably be sound (no conclusion derived
from the abstract semantics is wrong relative to the program concrete
semantics and specification). Otherwise stated, a proof that the
abstract semantics satisfies the abstract specification should imply
that the concrete semantics also satisfies the concrete specification.
Hoare logic is a sound verification method, debugging is not (since
some executions are left out), bounded model checking is not either
(since parts of some executions are left out). Unsound abstractions
lead to false negatives (the program may be claimed to be
correct/non erroneous with respect to the specification whereas it is
indeed incorrect).
Abstractions should also preferably be complete (no aspect of
the semantics relevant to the specification is left out). So if the
concrete semantics satisfies the concrete specification this should be
provable in the abstract. However program proofs are undecidable, and
so automatic tools for reasoning about programs are all incomplete
(for non trivial program properties such as safety, liveness, or
security) and must therefore fail on some programs. This can be
achieved by allowing the tool not to terminate, to be unsound (e.g. debugging tools omit possible executions), or to be incomplete (e.g. static analysis tools may produce false alarms). Incomplete
abstractions lead to false positives or false alarms
(the specification is claimed to be potentially violated by some
program executions while it is not).
Potentially nonterminating and unsound program verification tools are
easy to design. Terminating and sound tools are much more difficult
to design. Complete tools are impossible to design, by
undecidability. However static analysis tools producing very few or
no false alarms have been designed and used in industrial contexts for
specific families of properties and programs [42].
In all cases, abstract interpretation provides a systematic
construction method based on the effective approximation of the
concrete semantics, which can be (partly) automated and/or formally
verified.
Abstract interpretation aims at
 providing a basic coherent and conceptual theory for
understanding in a unified framework the thousands of ideas, concepts,
reasonings, methods, and tools on formal program analysis and
verification [22,26];
 guiding the correct formal design of automatic tools for program
analysis (computing an abstract semantics) and program
verification (proving that an abstract semantics satisfies an
abstract specification) [17].
Abstract interpretation theory studies semantics (formal models of
computer systems), abstractions, their soundness, and completeness.
The informal presentation
"Abstract
Interpretation in a Nutshell" aims at providing a short intuitive
introduction to the theory. The
"basic
concepts
of
abstract
interpretation" and an elementary
"course
on abstract interpretation" can also be found on the web.
2 What can be formalized by abstract interpretation?
Abstract interpretation is useful in computer science to formalize
reasonings involving the [sound [and complete]] approximation of the
semantics of formal systems. A nonexhaustive list of typical
examples of application is given below.
2.1 Syntax
The analysis of properties of grammars as well as parsing are abstract
interpretations of the grammar operational semantics and its
abstractions (such as parse trees, protolanguages, or terminal
languages) [39].
2.2 Semantics
The semantics of programs describes their possible runtime executions
in all possible execution environments at some level of abstraction.
The hierarchy of semantics, including trace, smallstep, and bigstep
operational semantics, relational semantics, denotational semantics,
predicate transformers, and axiomatic semantics in their angelic,
natural, and demoniac versions can be designed by abstract
interpretation [32,19]. An
extension to transfinite behaviors is useful to formalize e.g. semantic slicing [54].
2.3 Proofs
Formal proofs of program correctness involve an abstraction since
specifications always ignore some aspects of program execution which
need not be taken into account in the proof [18].
2.4 Static analysis
Static analysis is the automatic determination of abstract program
properties
[22,44,26,15]
including Dataflow Analysis
[67], [26,36],
Setbased Analysis [35], etc. This was
the motivating application behind the introduction of the abstract
interpretation theory.
Static typing and type inference [97] can be
understood as an abstract interpretation of runtime type checking thus
providing a "correct by construction" design method
[16,11].
2.6 Modelchecking
Modelchecking exhaustively verifies temporal properties on a
finite model of hardware or software computer systems
[10]. This abstraction of a system into a
model is often left implicit. Abstract model checking, as
formalized by abstract interpretation, makes this abstraction explicit
[9], [36], .
Modelchecking is reputed to be terminating, sound, and complete on the
model. From an abstract interpretation point of view, relating the
system to its model, it may be sound on the model but unsound on the
system (e.g. the model is correct for safety properties but wrong for
liveness properties), it is often incomplete (no finite model can
cover the specified behaviors of the system [100])
and, in practice, may explode combinatorially. In all cases abstract
interpretations of the system into a model have to be considered. All
transition models are abstract semantics but the converse is not true.
2.7 Predicate abstraction
Predicate abstraction [61] can be used to reduce any
static analysis on a finite abstract domain to boolean fixpoint
computations as performed by a modelchecker using a theorem prover to
automatically derive the abstract transformers involved in the
fixpoint definition. Parametric predicate abstraction is an extension
to infinite abstract domains [20].
2.8 Counterexamplebased refinement
Spurious counterexamplebased refinement in abstract modelchecking
is formalized as an abstract domain completion problem in the abstract
interpretation theory [56,43].
2.9 Strong Preservation
The problem of modifying finite abstract model checking by minimal
refinements in order to get strong preservation for some specification
language, including partition refinement algorithms, is a completion
problem in the abstract interpretation theory
[101].
2.10 Program transformation
Program transformations (such as partial evaluation
[72]) often require a static analysis of the
source program, as formalized by abstract interpretation (e.g. [71]). Moreover, the transformation itself, from source
to object programs, involves a loss of information on the original
program or a limitation on the possible program behaviors. This
approximation can be formalized by abstract interpretation. This was
exemplified on deadcode elimination, slicing, partial evaluation, or
program monitoring [38].
2.11 Watermarking
Looking for program watermarks that are not subject to obfuscation, one
can think to an abstract interpretation of the program semantics
[40].
2.12 Information hiding
In languagebased software security, the information to be hidden to an
intruder can be formalized as an abstract interpretation of the
program semantics [55].
2.13 Code obfuscation
The aim of code obfuscation is to prevent malicious users from
discovering properties of the original source program. This goal can
be precisely modeled by abstract interpretation, where the hiding of
properties corresponds to abstracting the semantics
[99].
2.14 Malware detection
An obfuscated malware is better detected by the effects of its
execution as recognized by an abstract interpretation rather than by a
syntactic signature [98].
2.15 Termination
A relational abstractinterpretationbased static analysis on a
wellfounded abstract domain can be systematically extended to a
termination analysis [3] (whence liveness analyses).
Termination analysis may require probabilistic hypotheses [87] or fairness hypotheses
on parallel processes [78].
3 Topics in abstract interpretation
3.1 Abstract domains
An abstract domain is an abstract algebra, often implemented as a
library module (see Sec. 5), providing a
description of abstract program properties and abstract property
transformers describing the operational effect of program instructions
and commands in the abstract. Abstract domains are often complete
lattices, an abstraction of powersets [26].
3.2 Finite versus infinite abstract domains
The first infinite abstract domain (that of intervals) was introduced
in [21]. This abstract domain was later used
to prove that, thanks to widenings, infinite abstract domains can lead
to effective static analyses for a given programming language that are
strictly more precise and equally efficient than any other one using a
finite abstract domain or an abstract domain satisfying chain
conditions [31].
3.3 Merge over all paths (MOP) in dataflow analysis
The
first dataflow analyses where proved correct by comparing the union of
the abstraction along all execution paths (socalled MOP^{1} solution) with a fixpoint solution
using transfer functions (i.e. abstract property transformer)
[67]. Instead of comparing one solution of the static
analysis problem to another one, the theory of abstract interpretation
introduced the idea that the correctness/soundness should be expressed
with respect to a formal semantics. A consequence is that static
analysis algorithms can be specified and designed by approximation of
a program semantics. Moreover, the "fixpoint solution" was shown to
be an abstraction of the "MOP solution". These two solutions coincide
for distributive abstract interpretations (for which abstract
transformers preserve union). Otherwise, the abstract domain used for
the fixpoint solution can be minimally enriched into its
disjunctive completion to get exactly the "MOP solution" in
fixpoint form (on the completed abstract domain)
[26].
3.4 Standard and collecting semantics
The collecting semantics or nonstandard semantics
(after the static semantics of [22]) is
the semantics of the language formally defining the program execution
properties of interest to be analyzed by abstraction. These program
executions themselves are formalized by the standard semantics.
For example in [22], the standard semantics is
an operational semantics. The concrete properties of interest are invariance
properties so the collecting semantics defines the reachable states
from initial states. This collecting semantics is expressed as the
least fixpoint of equations using strongest postcondition
transformers. Thus the considered abstractions provide abstract
invariance properties (overapproximating the reachable states).
3.5 Galois connection
Galois connections can be used when the abstract domain always offers
a most precise approximation of any concrete property
[26]. Indeed the Galois connections
introduced in [21,22] are
the semidual of the one introduced by Évariste Galois, and so do
compose (the abstraction of an abstraction is an abstraction).
Equivalent presentations involve closure operators, ideals,
congruences, etc [26].
An interesting consequence of the existence of the best abstraction of
concrete properties is the existence of best/most precise
transformers, which provides guidelines for their [automatic] design
[17]. Moreover by abstracting
fixpoints by fixpoints, static analysis is specified by an abstract
semantics expressed in fixpoint form whereas a static analyzer is an
algorithm for computing or overapproximating this fixpoint.
There are several alternative formalizations in absence of best
approximations [94], [30].
3.6 Moore family, Closure operators
If the correspondance between the concrete and abstract properties is
given by a Galois connection, then the image of the abstract
properties in the concrete is a Moore family, which is the
image of the concrete properties by a closure operator
[26]. The formalization of the abstraction by
closure operators is useful to abstract away from the representation
of the concrete properties. Other equivalent formalizations of the
existence of the best abstraction of concrete properties include
principal ideals, complete join congruences, etc
[26].
3.7 Moore completion
If an abstract domains has no best approximations for some concrete
properties its Moore completion is the most abstract abstract
domain more expressive than the original abstract domain which has
this property [26]. This introduces a Galois
connection.
3.8 Fixpoints
Most program properties can be expressed as fixpoints of monotone or
extensive property transformers, a property preserved by abstraction
[26]. This reduces program analysis to
fixpoint approximation and verification to fixpoint checking
[22].
3.9 Inference rules
Most (concrete and abstract) program properties can also be expressed
using inference rules, which indeed is equivalent to definitions
using fixpoints, equations, constraints, etc
[34]. This point of view has the advantage of
separating the design of an (abstract) semantics (or a static
analysis) from its formal presentation.
3.10 Iteration
A standard method for fixpoints construction is iteration. This can
be extended to transfinite iterations to prove Tarski's fixpoint
theorem [25]. In practice one can accelerate the
fixpoint computation using appropriate iteration strategies formalized
as chaotic/asynchronous iterations [14]. This
extends to higherorder
[24], [74].
3.11 Convergence acceleration by widening/narrowing
Convergence acceleration is mandatory in infinite abstract domains in
which the iterative computation of abstract fixpoints may diverge.
Widenings/narrowings and their duals are universal methods to do so
[22,14]. This extends to
higherorder [24,6].
3.12 Constraint resolution
Thanks to Tarski's theorem, fixpoints can be reexpressed as equality
or inequality constraints whence static analysis can be equally viewed
as a fixpoint approximation or as a constraint resolution problem.
Some constraint resolution methods are mere fixpoint iteration (e.g. setbased analysis [35]).
3.13 Modularity
The static analysis of programs by parts [37].
This includes separate interprocedural analysis
[24].
3.14 Abstract domain combination
The design of abstractions can be done by parts, by choosing basic
abstractions and then by composing them using abstract domain
combinators [26]. This provides a unifying
view on abstract domain design [52].
There are numerous examples of such abstract domain combinations
including the reduced sum, the reduced product and the
reduced power [26].
3.15 Refinement
The enrichment of an abstract domain so has to express in the refined
domain properties which cannot be expressed in the original domain.
Examples are the Moore completion Sec. 3.7, partitioning
[15,5,79], [69],
the disjunctive completion
[26], [53], the Heyting
completion [59],
complementation
[13], etc.
3.16 Completion
The refinement of an abstract domain into the most abstract abstract
domain which is precise enough to prove a given specification
[26], [93,57,58,104].
3.17 Lattice of abstract interpretations
A consequence of the formalization of static analyses by Galois
connections is that they can be organized into a complete lattice
according to the partial order of their relative precisions
[26]. All semantics and analyses are
present in this formally defined lattice and so it remains to find the
useful ones, which is the real question!
4 Examples of abstractinterpretationbased static analyses
4.1 Numerical Analysis
Contrary to dataflow analyses on lattices satisfying the
ascending/descending chain condition in the seventies, the
generalization to precise static analyses using numerical domains such
as intervals [21], octagons
[83] or polyhedra are
in infinite abstract domains whence required the introduction of new
wideningbased iteration convergence acceleration methods to become
effective.
4.2 Interval analysis
The analysis of the interval in which the values of variables do range
[21,22].
4.3 Octagonal analysis
The analysis of the octagon in which the values of pairs of variables
do range (that is the determination of constraints of the form +/x+/y ≤ c where x and y are variables and c a rational
constant automatically discovered by the analysis)
[83,84,85].
4.4 Polyhedral analysis
The analysis of the polyhedron in which the values of tuples of
variables do range. This abstract interpretation can be used for the
automatic discovery of invariant linear inequalities among numerical
variables of a program [44].
Delay analysis in synchronous programs [64], safety
analysis of reactive systems [65], quantitative time
properties of synchronous programs, and linear hybrid systems
[66] are among the many applications.
4.5 Congruence analysis
The analysis of the congruence invariants satisfied by the values of
one [62] or several numerical
variables [84].
4.6 Roundoff error analysis
The analysis of the origin of roundoff errors in floating point
computations [60,77].
4.7 Symbolic analysis
The analysis of symbolic properties of programs, usually as opposed to
numerical program properties e.g. heap reachability analysis
[23,24]. Also understood as the
symbolic representation of abstract domains, which is almost always
the case, since abstract properties cannot generally be simplistically
represented as the set of concrete values which have this property
(except in enumerative modelchecking [10]).
4.8 Strictness and comportment analysis
Strictness analysis determines whether a parameter in a lazy language
is always evaluated in a procedure call or this call does not
terminate. This information is useful to replace a callbyneed by a
more efficient call by value [91]. Introduced by Alan Mycroft
[92], this analysis was at the origin of the use of abstract
interpretation in the functional language community
[1,73]. Strictness analysis
[8,95] can be embedded in the lattice of
comportment analyses [33].
4.9 Mode inference/groundness/sharing analysis
The necessity of optimizing Prolog implementations, in particular the
occur checks during unification, is at the origin of the use of
abstract interpretation for the static analysis of Prolog
[80,45,107,75,76,90,7,12,2],
[29].
4.10 Aliasing and pointer analysis
The static analysis of imperative programs must take accesses and side
effects through aliases and pointers into account
[23]. The profuse literature on pointer analysis
is surveyed in [46,68].
4.11 Escape analysis
Escape analysis is a static analysis that determines whether the
lifetime of data exceeds its static scope
[96,47], [4].
4.12 Heap analysis
Heap analysis consists in overapproximating the sets of sequences of
graphs representing the memory heap at all time instants during
execution. Applications range from memory leak detection to
shape analysis that is the determination of the shape of data
structures allocated on the heap [103,102].
4.13 Concurrency analysis
The static analysis of concurrent programs from sharedmemory
[28] to [a]synchronous
communication [27], a vast and difficult
subject, with few analyses that do scale up.
4.14 Mobility analysis
The analysis of dynamically allocated mobile processes (such as the
picalculus). This involves the overapproximation of the set of
sequences of graphs representing the process allocations and
communications at all time instants during execution
[109,51].
4.15 Control flow analysis (CFA)
Control flow analysis aims at determining the possible flows of
computation in higherorder functional languages [70,106].
4.16 Probabilistic analysis
The static analysis of probabilistic programs
[86,88,89],
[48].
4.17 WCET analysis
The static determination of the worstcase execution time
[49] which involves the analysis of
the cache behavior [50], the pipelines, etc.
4.18 Hardware analysis
The static analysis of hardware formal descriptions
such as asynchronous circuits [108].
5 Libraries of abstract domains
The notion of abstract domain in abstract interpretation (see
Sec. 3.1) is independent of particular
applications and can be implemented in libraries which can be used as
parts of many different static analyses and even substituted for one
another. Such libraries implement a representation of abstract
properties and algorithms encoding operations on these properties such
as logical operations, property transformers, widenings, etc.
5.1 The NewPolka polyhedral library
The
NewPolka
library handles convex polyhedra, whose constraints and generators
have rational coefficients (with C and OCaml interfaces).
The Parma Polyhedra Library (PPL)
is a userfriendly, fully dynamic, portable, exceptionsafe, and
efficient C++ library to handle convex polyhedra that can be defined
as the intersection of a finite number of (open or closed)
hyperspaces, each described by an equality or inequality (strict or
nonstrict) with rational coefficients.
The Octagon Abstract Domain
Library is a library for manipulating special kinds of polyhedra
called octagons that correspond to sets of constraints of the form
+/x +/y ≤ c (where x and y are variables and c a rational
constant and so, in dimension two, these polyhedra have at most eight
faces) [85].
6 Abstractinterpretationbased tools
The following list of static analysis and verification automatic tools
provides an idea of the scope of practical applications of abstract
interpretation to software verification (but this list is definitely
not exhaustive). These tools aim at soundness. Since no universal
tool can exist (because of undecidability) such tools are necessarily
incomplete and vary in their capacity to produce very few false alarms and to
scale up to very large programs.
A static analyzer from the Programming
Research
Laboratory of the
Seoul
National
University and
RopasWork for automatic detection of
buffer overrun errors in C programs.
Commercial static analyzers from AbsInt
Angewandte Informatik to statically compute tight bounds for the
worstcase execution time (WCET) of tasks in realtime systems.
A static analyzer from the École normale
supérieure for proving the absence of runtime errors specialized
for synchronous control/command programs written in C.
A research prototype static analyzer from the
Intelligent
Systems
Division
at the
NASA
Ames
Research
Center for finding runtime errors in C
programs.
A static analyzer from CEALIST to
study the propagation of rounding errors in floatingpoint
computations of C or assembler programs.
A commercial generalpurpose static analyzer of
PolySpace Technologies for detecting
runtime errors in Ada, C, C++, and Java.
A static analyzer from
Microsoft
Research Cambridge for proving program termination and general
liveness properties of C programs.
TVLA is a research tool developed at
Tel Aviv University for experimenting
with abstract interpretation using a logical description of program
semantics with a predefined abstraction of predicates.
7 Conferences with abstract interpretation sessions
 Generalist conferences:
 Specialized conferences:
8 Short bibliography
 [1]

S. Abramsky & C. Hankin, editors. 
Abstract
Interpretation
of
Declarative
Languages. 
Ellis Horwood, 1987, Computers and their Applications.
 [2]

R. Barbuti, R. Giacobazzi & G. Levi. 
A
General
Framework
for
Semanticsbased
Bottomup
Abstract
Interpretation
of
Logic
Programs.
TOPLAS, Vol. 15, n&86; 1, Jan. 1993, pp.
133181.
 [3]

J. Berdine, A. Chawdhary, B. Cook, D. Distefano & P. O'Hearn. 
Variance
analyses
from
invariance
analyses. In :
34^{th} POPL, edited by M. F. Martin Hofmann, Nice,
FR, 2007. pp. 211224. 
ACM Press.
 [4]

B. Blanchet. 
Escape
Analysis
for
Java^{TM}.
Theory
and
Practice. TOPLAS, Vol. 25, n&86; 6, Nov. 2003, pp.
713775.
 [5]

F. Bourdoncle. 
Abstract
Interpretation
by
Dynamic
Partitioning.
J. Func. Prog., Vol. 2, n&86; 4, 1992, pp.
407435.
 [6]

F. Bourdoncle. 
Efficient
Chaotic
Iteration
Strategies
with
Widenings.
In : Proc. FMPA, edited by D. Bjørner, M. Broy & I. Pottosin. Akademgorodok, Novosibirsk, RU, LNCS 735, pp.
128141. 
Springer, 28 June 2 Jul. 1993.
 [7]

M. Bruynooghe. 
A
Practical
Framework
for
the
Abstract
Interpretation
of
Logic
Programs. J. Logic Programming,
Vol. 10, n&86; 1,2,3&4, Jan. 1991, pp. 91124.
 [8]

G. Burn, C. Hankin & S. Abramsky. 
Strictness
Analysis
of
HigherOrder
Functions. Sci.
Comput. Programming, Vol. 7, Nov. 1986, pp. 249278.
 [9]

E. Clarke, O. Grumberg & D. Long. 
Model
Checking
and
Abstraction.
TOPLAS, Vol. 16, n&86; 5, Sep. 1994, pp.
15121542.
 [10]

E. Clarke, O. Grumberg & D. Peled. 
Model
Checking. 
MIT Press, 1999.
 [11]

M. Comini, F. Damiani & S. Vrech. 
On polymorphic recursion, type systems, and abstract interrpetation.
In : Proc. 15^{th} Int. Symp.
SAS '08, edited by M. Alpuente & G. Vidal, pp. 144158.

Springer, 2008, Valencia, ES, 1618 Jul. 2008, LNCS 5079.
 [12]

A. Cortesi & G. Filé. 
Abstract
interpretation
of
logic
programs:
an
abstract
domain
for
groundness,
sharing,
freeness
and
compoundness
analysis.
In : Proc. PEPM '91, edited by P. Hudak & N. Jones, pp. 5261. 
ACM Press, Sep. 1991, Yale U., New Haven, CT, US, 1719 June
1991, ACM SIGPLAN Not. 26(9).
 [13]

A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi & F. Ranzato. 
Complementation
in Abstract
Interpretation. TOPLAS, Vol. 19, n&86; 1, Jan.
1997, pp. 747.
 [14]

P. Cousot. 
Méthodes itératives de construction et
d'approximation de points fixes d'opérateurs
monotones sur un treillis, analyse sémantique de
programmes (in French). 
Grenoble, FR, Thèse d'État ès sciences
mathématiques, Université scientifique et
médicale de Grenoble, 21 Mar. 1978.
 [15]

P. Cousot. 
Semantic
Foundations
of
Program
Analysis,
invited
chapter.
In : Program Flow Analysis: Theory and Applications,
edited by S. Muchnick & N. Jones, Chapter 10, pp.
303342. 
PrenticeHall, 1981.
 [16]

P. Cousot. 
Types
as
Abstract
Interpretations, invited
paper.
In : 24^{th} POPL, Paris, FR, Jan. 1997.
pp. 316331. 
ACM Press.
 [17]

P. Cousot. 
The
Calculational
Design of
a
Generic
Abstract
Interpreter,
invited
chapter. In : Calculational System Design, edited by
M. Broy & R. Steinbrüggen, pp. 421505. 
NATO Science Series, Series F: Computer and Systems Sciences. IOS
Press, 1999, Volume 173.
 [18]

P. Cousot. 
Partial
Completeness
of
Abstract
Fixpoint
Checking,
invited
paper.
In : Proc. 4^{th} Int. Symp.
SARA '2000, edited by B. Choueiry & T. Walsh, pp. 125.

Springer, 2629 Jul. 2000, Horseshoe Bay, TX, US, LNAI
1864.
 [19]

P. Cousot. 
Constructive
Design
of
a
Hierarchy
of
Semantics
of
a
Transition
System
by
Abstract
Interpretation. Theoret. Comput. Sci., Vol. 277, n&86;
12, 2002, pp. 47103.
 [20]

P. Cousot. 
Verification
by
Abstract
Interpretation, invited
chapter.
In : Proc. Int. Symp. on Verification  Theory &
Practice  Honoring Zohar Manna's 64th Birthday, edited by
N. Dershowitz, pp. 243268. 
Taormina, IT, LNCS 2772, Springer, 29 June  4 Jul. 2003.
 [21]

P. Cousot & R. Cousot. 
Static
determination
of
dynamic
properties
of
programs.
In : Proc. 2^{nd} Int. Symp. on
Programming, Paris, FR, 1976. pp. 106130. 
Dunod.
 [22]

P. Cousot & R. Cousot. 
Abstract
interpretation: a
unified
lattice
model
for
static
analysis
of
programs
by
construction
or
approximation
of
fixpoints.
In : 4^{th} POPL, Los Angeles, CA, 1977. pp.
238252. 
ACM Press.
 [23]

P. Cousot & R. Cousot. 
Static
determination
of
dynamic
properties
of
generalized
type
unions.
In : ACM Symposium on Language Design for Reliable
Software, Raleigh, NC, ACM SIGPLAN Not. 12(3):7794, 1977.
 [24]

P. Cousot & R. Cousot. 
Static
determination
of
dynamic
properties
of
recursive
procedures.
In : IFIP Conf. on Formal Description of Programming
Concepts, StAndrews, N.B., CA, edited by E. Neuhold. pp. 237277. 
NorthHolland, 1977.
 [25]

P. Cousot & R. Cousot. 
Constructive versions
of
Tarski's
fixed
point
theorems.
Pacific J. Math., Vol. 82, n&86; 1, 1979, pp.
4357.
 [26]

P. Cousot & R. Cousot. 
Systematic
design
of
program
analysis
frameworks.
In : 6^{th} POPL, San Antonio, TX, 1979. pp.
269282. 
ACM Press.
 [27]

P. Cousot & R. Cousot. 
Semantic
analysis
of
communicating
sequential
processes.
In : 7^{th} ICALP, edited by
J. de Bakker & J. van Leeuwen. LNCS 85, pp. 119133. 
Springer, Jul. 1980.
 [28]

P. Cousot & R. Cousot. 
Invariance
Proof
Methods
and
Analysis
Techniques
For
Parallel
Programs,
invited
chapter.
In : Automatic Program Construction Techniques,
edited by A. Biermann, G. Guiho & Y. Kodratoff,
Chapter 12, pp. 243271. 
Macmillan, 1984.
 [29]

P. Cousot & R. Cousot. 
Abstract
Interpretation
and
Application
to
Logic
Programs.
J. Logic Programming, Vol. 13, n&86; 23, 1992,
pp. 103179. 
(The editor of J. Logic Programming has mistakenly
published the unreadable galley proof. For a correct version of this paper,
see http://www.di.ens.fr/~cousot.).
 [30]

P. Cousot & R. Cousot. 
Abstract
Interpretation
Frameworks.
J. Logic and Comp., Vol. 2, n&86; 4, Aug.
1992, pp. 511547.
 [31]

P. Cousot & R. Cousot. 
Comparing
the
Galois
Connection
and
Widening/Narrowing
Approaches
to
Abstract
Interpretation, invited
paper.
In : Proc. 4^{th} Int. Symp. on
PLILP '92, edited by M. Bruynooghe & M. Wirsing.
Leuven, BE, 2628 Aug. 1992, LNCS 631, pp. 269295. 
Springer, 1992.
 [32]

P. Cousot & R. Cousot. 
Inductive
Definitions,
Semantics
and
Abstract
Interpretation. In : 19^{th} POPL, Albuquerque, NM, US,
1992. pp. 8394. 
ACM Press.
 [33]

P. Cousot & R. Cousot. 
HigherOrder
Abstract
Interpretation
(and
Application
to
Comportment
Analysis
Generalizing
Strictness,
Termination,
Projection
and
PER
Analysis
of
Functional
Languages),
invited
paper.
In : Proc. 1994 ICCL, Toulouse, FR, 1619 May 1994.
pp. 95112. 
IEEE Comp. Soc. Press.
 [34]

P. Cousot & R. Cousot. 
Compositional
and
Inductive
Semantic
Definitions
in
Fixpoint,
Equational,
Constraint,
Closurecondition, Rulebased
and
GameTheoretic
Form,
invited
paper.
In : Proc. 7^{th} Int. Conf.
CAV '95, edited by P. Wolper. Liège, BE, LNCS 939,
pp. 293308. 
Springer, 35 Jul. 1995.
 [35]

P. Cousot & R. Cousot. 
Formal
Language,
Grammar
and
SetConstraintBased
Program
Analysis
by
Abstract
Interpretation. In : Proc. 7^{th} FPCA, La Jolla, CA, US,
2528 June 1995. pp. 170181. 
ACM Press.
 [36]

P. Cousot & R. Cousot. 
Temporal
Abstract
Interpretation. In : 27^{th} POPL, Boston, MA, US, Jan.
2000. pp. 1225. 
ACM Press.
 [37]

P. Cousot & R. Cousot. 
Modular
Static
Program
Analysis,
invited
paper.
In : Proc. 11^{th} Int. Conf.
CC '2002, edited by R. Horspool, Grenoble, FR, 614 Apr. 2002.
pp. 159178. 
LNCS 2304, Springer.
 [38]

P. Cousot & R. Cousot. 
Systematic
Design
of
Program
Transformation
Frameworks
by
Abstract
Interpretation. In : 29^{th} POPL, Portland, OR, US, Jan.
2002. pp. 178190. 
ACM Press.
 [39]

P. Cousot & R. Cousot. 
Parsing
as
Abstract Interpretation
of
Grammar
Semantics. Theoret. Comput. Sci., Vol. 290, n&86; 1,
Jan. 2003, pp. 531544.
 [40]

P. Cousot & R. Cousot. 
An
Abstract
InterpretationBased
Framework
for
Software
Watermarking.
In : 31^{st} POPL, Venice, IT, 1416 Jan.
2004. pp. 173185. 
ACM Press.
 [41]

P. Cousot & R. Cousot. 
Grammar
Analysis
and
Parsing
by
Abstract
Interpretation,
invited
chapter. In : Program Analysis and Compilation, Theory
and Practice: Essays dedicated to Reinhard Wilhelm, edited by T. Reps,
M. Sagiv & J. Bauer, pp. 178203. 
Springer, 2006, LNCS 4444.
 [42]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux & X. Rival. 
The
ASTRéE analyser.
In : Proc. 14^{th} ESOP '2005, Edinburg,
UK, edited by M. Sagiv, pp. 2130. 
Springer, 210 Apr. 2005, LNCS, Vol. 3444.
 [43]

P. Cousot, P. Ganty & J.F. Raskin. 
FixpointGuided Abstraction
Refinements.
In : Proc. 14^{th} Int. Symp.
SAS '07, edited by G. Filé & H. RiisNielson, pp.
333348. 
Springer, 2224 Aug. 2007, Kongens Lyngby, DK, LNCS 4634.
 [44]

P. Cousot & N. Halbwachs. 
Automatic
discovery
of
linear
restraints
among
variables
of
a
program.
In : 5^{th} POPL, Tucson, AZ, 1978. pp.
8497. 
ACM Press.
 [45]

S. Debray & D. Warren. 
Automatic
mode
inferencing
for
Prolog
programs. In :
Proc. 1986 Int. Symp. on Logic Programming, pp. 7888. 
IEEE Comp. Soc. Press, Sep. 1986, Salt Lake City, UT.
 [46]

A. Deutsch. 
Semantic
models
and
abstract
interpretation
techniques
for
inductive
data
structures
and
pointers,
,
invited
paper. In : Proc.
PEPM '95, La Jolla, CA, 2123 June 1995. pp. 226229. 
ACM Press.
 [47]

A. Deutsch. 
On
the
complexity
of
escape
analysis.
In : 24^{th} POPL, Paris, FR, Jan. 1997.
pp. 358371. 
ACM Press.
 [48]

A. Di Pierro, C. Hankin & H. Wiklicky. 
Probabilistic lambda calculus and quantitative program analysis.
J. Logic and Comp., Vol. 15, n&86; 2, 2005, pp.
159179.
 [49]

C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt, H. Theiling,
S. Thesing & R. Wilhelm. 
Reliable
and
Precise
WCET
Determination
for
a
RealLife
Processor. In : Proc.
1^{st} Int. Work. EMSOFT '2001, edited by
T. Henzinger & C. Kirsch, pp. 469485. 
Springer, 2001, LNCS, Vol. 2211.
 [50]

C. Ferdinand, F. Martin, R. Wilhelm & M. Alt. 
Cache behavior prediction by abstract interpretation. Sci.
Comput. Programming, Vol. 35, n&86; 1, 1999, pp.
163189.
 [51]

J. Feret. 
Abstract
InterpretationBased Static
Analysis
of
Mobile
Ambients.
In : Proc. 8^{th} Int. Symp.
SAS '01, edited by P. Cousot. Paris, FR, LNCS 2126, pp.
413431. 
Springer, 1618 Jul. 2001.
 [52]

G. Filè, R. Giacobazzi & F. Ranzato. 
A
Unifying
View
on
Abstract
Domain Design. ACM Computing Surveys, Vol. 28, n&86; 2, 1996,
pp. 333336.
 [53]

G. Filé & F. Ranzato. 
The
Powerset
Operator
on
Abstract
Interpretations.
Theoret. Comput. Sci., Vol. 222, n&86; 12,
Jul. 1999, pp. 77111.
 [54]

R. Giacobazzi & I. Mastroeni. 
NonStandard
Semantics
for
Program
Slicing. HigherOrder
and Symbolic Computation, Vol. 16, n&86; 4, 2003, pp.
297339.
 [55]

R. Giacobazzi & I. Mastroeni. 
Timed Abstract
NonInterference. In : Proc. 3^{rd} Int. Conf.
FORMATS '05, edited by B. Le Charlier, pp. 289303. 
Springer, 2005, Uppsala, SE, 2628 Sep. 2005, LNCS 3829.
 [56]

R. Giacobazzi & E. Quintarelli. 
Incompleteness,
Counterexamples
and
Refinements
in
Abstract
ModelChecking. In : Proc. 8^{th} Int. Symp.
SAS '01, edited by P. Cousot. Paris, FR, LNCS 2126, pp.
356373. 
Springer, 1618 Jul. 2001.
 [57]

R. Giacobazzi & F. Ranzato. 
Completeness
in
Abstract
Interpretation:
A
Domain
Perspective. In : Proc. 6^{th} Int. Conf.
AMAST '97, Sydney, AU, edited by M. Johnson. LNCS,
Vol. 1349, pp. 231245. 
Springer, 1318 Dec. 1997.
 [58]

R. Giacobazzi, F. Ranzato & F. Scozzari. 
Making
Abstract Interpretations
Complete. J. ACM, Vol. 47, n&86; 2, 2000, pp. 361416.
 [59]

R. Giacobazzi & F. Scozzari. 
A
logical
model
for
relational
abstract
domains.
TOPLAS, Vol. 20, n&86; 5, 1998, pp. 10671109.
 [60]

É. Goubault, M. Martel & S. Putot. 
Asserting the precision of floatingpoint computations: a simple
abstract interpreter. In : Proc. 11^{th}
ESOP '2002, edited by D. Le Métayer, pp. 209212. 
Springer, 812 Apr. 2002, Grenoble, FR, LNCS 2305.
 [61]

S. Graf & H. Saïdi. 
Verifying
Invariants
Using
Theorem
Proving.
In : Proc. 8^{th} Int. Conf.
CAV '97, edited by R. Alur & T. Henzinger. New
Brunswick, NJ, US, LNCS 1102, pp. 196207. 
Springer, Jul. 31  Aug. 3 1996.
 [62]

P. Granger. 
Static
Analysis
of
Arithmetical
Congruences.
Int. J. Comput. Math., Vol. 30, 1989, pp.
165190.
 [63]

P. Granger. 
Static
Analysis
of
Linear
Congruence
Equalities
among
Variables
of
a
Program. In :
Proc. Int. J. Conf. TAPSOFT '91, Volume 1 (CAAP '91),
edited by S. Abramsky & T. Maibaum. Brighton, GB, LNCS
493, pp. 169192. 
Springer, 1991.
 [64]

N. Halbwachs. 
Delay
Analysis
in
Synchronous
Programs.
In : Proc. 5^{th} Int. Conf.
CAV '93, edited by C. Courcoubatis. Elounda, GR, LNCS 697,
pp. 333346. 
Springer, 28 June 1 Jul. 1993.
 [65]

N. Halbwachs. 
About
Synchronous
Programming
and
Abstract
Interpretation.
In : Proc. 1^{st} Int. Symp.
SAS '94, edited by B. Le Charlier, pp. 179192. 
Springer, 1994, Namur, BE, 2022 Sep. 1994, LNCS 864.
 [66]

N. Halbwachs, Y. Proy & P. Roumanoff. 
Verification
of
realtime
systems
using
linear
relation
analysis.
Formal Methods in System Design, Vol. 11, n&86; 2,
Aug. 1997, pp. 157185.
 [67]

M. Hecht. 
Flow Analysis of Computer Programs. 
NorthHolland/Elsevier, 1977.
 [68]

M. Hind. 
Pointer
Analysis:
Haven't
We
Solved
This
Problem
Yet? In :
2001 ACM SIGPLANSIGSOFT Workshop PASTE '01, Snowbird, UT,
US, 2001.
 [69]

B. Jeannet, N. Halbwachs & P. Raymond. 
Dynamic
Partitioning
in
Analyses
of
Numerical
Properties.
In : Proc. 6^{th} Int. Symp.
SAS '99, edited by A. Cortesi & G. Filé, pp. 1838.

Springer, 1999, Venice, IT, 2224 Sep. 1999, LNCS
1694.
 [70]

N. Jones. 
Flow
Analysis
of
Lambda
Expressions
(Preliminary
Version). In : 8^{th} ICALP,
edited by S. Even & O. Kariv. LNCS 115, pp. 114128.

Springer, Jul. 1981.
 [71]

N. Jones. 
Combining
Abstract
Interpretation
and
Partial
Evaluation
(Brief
Overview).
In : Proc. 4^{th} Int. Symp.
SAS '97, edited by P. Van Hentenryck, pp. 396405. 
Springer, 1997, Paris, FR, 810 Sep. 1997, LNCS 1302.
 [72]

N. Jones, C. Gomard & P. Sestoft. 
Partial Evaluation and Automatic Program Generation. 
PrenticeHall, June 1993, Int. Series in
Computer Science.
 [73]

N. Jones & F. Nielson. 
Abstract
interpretation: a
semanticsbased tool
for
program
analysis.
In : Semantic Modelling, edited by S. Abramsky,
D. Gabbay & T. Maibaum, Chapter 5, pp. 527636. 
Clarendon Press, 1995, Handbook of Logic in Computer Science,
Vol. 4.
 [74]

N. Jones & M. Rosendahl. 
HigherOrder
Minimal
Function
Graphs.
J. Func. and Logic Prog., Vol. 1997, n&86; 2,
Feb. 1997.
 [75]

H. Mannila & E. Ukkonen. 
Flow
analysis
of
Prolog
programs.
In : Proc. 1987 Int. Symp. on Logic Programming.
San Francisco, CA, pp. 205214. 
IEEE Comp. Soc. Press, 31 Aug.  4Sep. 1987.
 [76]

K. Marriott & H. Søndergaard. 
BottomUp
Abstract
Interpretation
of
Logic
Programs.
In : Proc. 5^{th} Int. Conf. & Symp.
on Logic Programming, Volume 1, edited by R. Kowalski,name
K. Bowen. Seattle, WA, US, pp. 733748. 
MIT Press, 1519 Aug. 1988.
 [77]

M. Martel. 
An
Overview
of
Semantics
for
the
Validation
of
Numerical
Programs.
In : Proc. 6^{th} Int. Conf. VMCAI
2005, edited by R. Cousot, Paris, FR, 1719 Jan. 2005. pp.
5977. 
LNCS 3385, Springer.
 [78]

L. Mauborgne. 
Tree
Schemata
and
Fair
Termination.
In : Proc. 7^{th} Int. Symp.
SAS '2000, edited by J. Palsberg, pp. 302321. 
Springer, 29 June  1 Jul. 2000, Santa Barbara, CA, US, LNCS
1824.
 [79]

L. Mauborgne & X. Rival. 
Trace
Partitioning
in
Abstract
Interpretation
Based
Static
Analyzer.
In : Proc. 14^{th} ESOP '2005, Edinburg,
UK, edited by M. Sagiv, pp. 520. 
Springer, Apr. 2Ñ10, 2005, LNCS, Vol. 3444.
 [80]

C. Mellish. 
Abstract
Interpretation
of
Prolog
Programs.
In : 3^{rd} ICLP '86, edited by
E. Shapiro, pp. 463474. 
Springer, 1418 Jul. 1986, London, GB, LNCS 225.
 [81]

J. Midtgaard & T. Jensen. 
A calculational approach to controlflow analysis by abstract
interrpetation. In : Proc. 15^{th} Int.
Symp. SAS '08, edited by M. Alpuente & G. Vidal, pp.
347362. 
Springer, 2008, Valencia, ES, 1618 Jul. 2008, LNCS 5079.
 [82]

M. Might & . Shivers. 
Analyzing
the
environment
structure
of
higherorder
languages
using
frame
strings.
Theoret. Comput. Sci., Vol. 375, n&86; 13,
2007, pp. 137168.
 [83]

A. Miné. 
A
New
Numerical
Abstract
Domain
Based
on
DifferenceBound
Matrices.
In : Proc. 2^{nd} Symp. PADO '2001,
edited by . Danvy & A. Filinski. Århus, DK, 2123
May 2001, LNCS 2053, pp. 155172. 
Springer, 2001.
 [84]

A. Miné. 
A
Few
GraphBased
Relational
Numerical
Abstract
Domains.
In : Proc. 9^{th} Int. Symp.
SAS '02, edited by M. Hermenegildo & G. Puebla.
LNCS, Vol. 2477, pp. 117132. 
Springer, 2002.
 [85]

A. Miné. 
The
Octagon
Abstract
Domain.
HigherOrder and Symbolic Computation, Vol. 19, 2006,
pp. 31100.
 [86]

D. Monniaux. 
Abstract
interpretation of
probabilistic semantics.
In : Proc. 7^{th} Int. Symp.
SAS '2000, edited by J. Palsberg, pp. 322339. 
Springer, 29 June  1 Jul. 2000, Santa Barbara, CA, US, LNCS
1824.
 [87]

D. Monniaux. 
An
Abstract
Analysis
of
the
Probabilistic Termination
of
Programs.
In : Proc. 8^{th} Int. Symp.
SAS '01, edited by P. Cousot. Paris, FR, LNCS 2126, pp.
111127. 
Springer, 1618 Jul. 2001.
 [88]

D. Monniaux. 
An
Abstract
MonteCarlo Method
for
the
Analysis
of
Probabilistic Programs
(extended
abstract).
In : 28^{th} POPL, London, GB, Jan. 2001.
pp. 93101. 
ACM Press.
 [89]

D. Monniaux. 
Backwards
abstract
interpretation of
probabilistic programs.
In : Proc. 10^{th} ESOP '2001,
edited by D. Sands. Genova, IT, 26 Apr. 2001, LNCS 2028, pp.
367382. 
Springer, 2001.
 [90]

K. Muthukumar & M. Hermenegildo. 
Determination
of
Variable
Dependence
Information
through
Abstract
Interpretation.
In : NACLP 1989, Volume 1, edited by E. Lusk & R. Overbeek. Cleaveland, OH, US, pp. 166185. 
MIT Press, 1620 Oct. 1989.
 [91]

A. Mycroft. 
The
theory
and
practice
of
transforming
callbyneed
into
callbyvalue. In : Proc. 4^{th} Int. Symp. on
Programming, edited by B. Robinet, pp. 270281. 
Springer, 1980, Paris, FR, 2224 Apr. 1980, LNCS 83.
 [92]

A. Mycroft. 
Abstract
Interpretation
and
Optimising
Transformations
for
Applicative
Programs. 
Edinburg, UK, Ph.D. Dissertation, CST1581, Department of
Computer Science, University of Edinburgh, Dec. 1981.
 [93]

A. Mycroft. 
Completeness
and
predicatebased
abstract
interpretation. In : Proc. PEPM '93. Copenhagen,
DK, 1416 June 1993, pp. 8087. 
ACM Press, 1993.
 [94]

A. Mycroft & N. Jones. 
A
Relational
Framework
for
Abstract
Interpretation.
In : Programs as Data Objects, Proceedings of a Workshop,
edited by N. Jones & H. Ganzinger, pp. 156171. 
Springer, 1986, Copenhagen, DK, 1719 Oct. 1985, LNCS 215.
 [95]

F. Nielson. 
Strictness
Analysis
and
Denotational
Abstract
Interpretation. In : 14^{th}
POPL, Munchen, DE, 1987. pp. 120131. 
ACM Press.
 [96]

Y. G. Park & B. Goldberg. 
Escape
analysis
on
lists. In :
Proc. ACM SIGPLAN '92 Conf. PLDI. ACM SIGPLAN Not. 31(5),
San Francisco, CA, US, 2124, May 1992. pp. 116127. 
ACM Press.
 [97]

B. Pierce. 
Types
and
Programming
Languages. 
MIT Press, 2002.
 [98]

M. D. Preda, M. Christodorescu, S. Jha & S. Debray. 
SemanticsBased
Approach
to
Malware
Detection. In : 34^{th} POPL, Nice, France, 1719
Jan. 2007. pp. 238252. 
ACM Press.
 [99]

M. D. Preda & R. Giacobazzi. 
Control
Code
Obfuscation
by
Abstract
Interpretation.
In : Proc. 3^{rd} IEEEInt. Conf.
SEFM '05, Koblenz, DE, 2005. 
IEEE Comp. Soc. Press.
 [100]

F. Ranzato. 
On
the
Completeness
of
Model
Checking.
In : Proc. 10^{th} ESOP '2001,
edited by D. Sands. Genova, IT, 26 Apr. 2001, LNCS 2028, pp.
137154. 
Springer, 2001.
 [101]

F. Ranzato & F. Tapparo. 
Strong
Preservation
of
Temporal
FixpointBased
Operators
by
Abstract
Interpretation.
In : Proc. 7^{th} Int. Conf. VMCAI
2006, edited by A. Emerson & K. Namjoshi, Charleston, SC,
US, 810 Jan. 2006. pp. 332347. 
LNCS 3855 , Springer.
 [102]

N. Rinetzky, J. Bauer, T. Reps, S. Sagiv & R. Wilhelm. 
A
semantics for
procedure local
heaps
and
its
abstractions. In : 32^{nd} POPL, Long Beach, CA, US,
2005. pp. 296309. 
ACM Press.
 [103]

M. Sagiv, T. Reps & R. Wilhelm. 
Shape
Analysis.
In : Proc. Int. Conf. CC '2000, LNCS 1781,
edited by D. A. Watt, Berlin, DE, 25 Mar.  2 Apr. 2000. pp.
117. 
Springer.
 [104]

D. Schmidt. 
Comparing
completeness
properties
of
static
analyses
and
their
logics.
In : Proc. 4^{th} APLAS '2006,
edited by N. Kobayashi, Sydney, AU, 810 Nov. 2006. pp.
183199. 
LNCS 4279, Springer.
 [105]

O. Shivers. 
ControlFlow
Analysis
in
Scheme. In : Proc. ACM SIGPLAN '1988
Conf. PLDI. ACM SIGPLAN Not. 23(7), Atlanta, GE, US, 2224 June
1988. pp. 164174. 
ACM Press.
 [106]

O. Shivers. 
Higherorder
controlflow
analysis
in
retrospect:
lessons
learned,
lessons
abandoned. ACM SIGPLAN Not.,
Vol. 39, n&86; 4, 2004, pp. 257269.
 [107]

H. Søndergaard. 
An
Application
of
Abstract
Interpretation
of
Logic
Programs:
Occur
Check
Reduction.
In : Proc. ESOP '86, edited by B. Robinet & R. Wilhelm, pp. 327338. 
Springer, 1986, Saarbrücken, DE, 1719 Mar. 1986,
LNCS 213.
 [108]

S. Thompson & A. Mycroft. 
Abstract
Interpretation
of
Combinational
Asynchronous
Circuits.
In : Proc. 11^{th} Int. Symp.
SAS '04, edited by R. Giacobazzi. Verona, IT, LNCS 3148,
pp. 181196. 
Springer, 2628 Aug. 2004.
 [109]

A. Venet. 
Automatic
Determination
of
Communication
Topologies
in
Mobile
Systems.
In : Proc. 5^{th} Int. Symp.
SAS '98, edited by G. Levi, pp. 152167. 
Springer, 1998, Pisa, IT, 1416 Sep. 1998, LNCS 1503.
PDF version.
This document is hopefully sound, may be too abstract and necessarily
incomplete. Amendments are welcomed at
Patrick.Cousot@ens.fr.
Footnotes:
^{1}MOP
often stands for "Meet Over all Path" where the abstract meet
corresponds to a concrete join, the order in dataflow analysis often
being the inverse of the one used in abstract interpretation, whence
corresponds to a concrete inverse logical implication, which may
sometimes be counterintuitive.