Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Abstract Interpretation

Abstract Interpretation

Web page maintained by P. Cousot

Last update: Oct 3, 2006

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 Types
    2.6 Model-checking
    2.7 Predicate abstraction
    2.8 Counter-example-based refinement
    2.9 Strong Preservation
    2.10 Program transformation
    2.11 Watermarking
    2.12 Information hiding
    2.13 Code obfuscation
    2.14 Malware detection
    2.15 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 abstract-interpretation-based 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 Mode inference/groundness/sharing analysis
    4.10 Aliasing and pointer analysis
    4.11 Escape analysis
    4.12 Heap analysis
    4.13 Concurrency analysis
    4.14 Mobility analysis
    4.15 Control flow analysis (CFA)
    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 Abstract-interpretation-based 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 Conferences with abstract interpretation sessions
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 [21,25] 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 non-terminating 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 [40]. 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 [21,25];
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) [16].

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 non-exhaustive 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) [38].

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, small-step, and big-step operational semantics, relational semantics, denotational semantics, predicate transformers, and axiomatic semantics in their angelic, natural, and demoniac versions can be designed by abstract interpretation [31,18]. An extension to transfinite behaviors is useful to formalize e.g. semantic slicing [51].

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 [17].

2.4 Static analysis

Static analysis is the automatic determination of abstract program properties [21,41,25,14] including Dataflow Analysis [64], [25,35], Set-based Analysis [34], etc. This was the motivating application behind the introduction of the abstract interpretation theory.

2.5 Types

Static typing and type inference [92] can be understood as an abstract interpretation of runtime type checking thus providing a "correct by construction" design method [15].

2.6 Model-checking

Model-checking 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], [35], .

Model-checking 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 [95]) 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 [58] can be used to reduce any static analysis on a finite abstract domain to boolean fixpoint computations as performed by a model-checker 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 [19].

2.8 Counter-example-based refinement

Spurious counter-example-based refinement in abstract model-checking is formalized as an abstract domain completion problem in the abstract interpretation theory [53].

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 [96].

2.10 Program transformation

Program transformations (such as partial evaluation [69]) often require a static analysis of the source program, as formalized by abstract interpretation (e.g. [68]). 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 dead-code elimination, slicing, partial evaluation, or program monitoring [37].

2.11 Watermarking

Looking for program watermarks that are not subject to obfuscation, one can think to an abstract interpretation of the program semantics [39].

2.12 Information hiding

In language-based software security, the information to be hidden to an intruder can be formalized as an abstract interpretation of the program semantics [52].

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 [94].

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 [93].

2.15 Termination

A relational abstract-interpretation-based static analysis on a well-founded abstract domain can be systematically extended to a termination analysis [3] (whence liveness analyses). Termination analysis may require probabilistic hypotheses [81] or fairness hypotheses on parallel processes [75].

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 [25].

3.2 Finite versus infinite abstract domains

The first infinite abstract domain (that of intervals) was introduced in [20]. 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 [30].

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 (so-called MOP¹ solution) with a fixpoint solution using transfer functions (i.e. abstract property transformer) [64]. 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) [25].

3.4 Standard and collecting semantics

The collecting semantics or non-standard semantics (after the static semantics of [21]) 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 [21], 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 [25]. Indeed the Galois connections introduced in [20,21] are the semi-dual 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 [25].

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 [16]. 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 [89], [29].

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 [25]. 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 [25].

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 [25]. 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 [25]. This reduces program analysis to fixpoint approximation and verification to fixpoint checking [21].

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 [33]. 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 [24]. In practice one can accelerate the fixpoint computation using appropriate iteration strategies formalized as chaotic/asynchronous iterations [13]. This extends to higher-order [23], [71].

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 [21,13]. This extends to higher-order [23,6].

3.12 Constraint resolution

Thanks to Tarski's theorem, fixpoints can be re-expressed 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. set-based analysis [34]).

3.13 Modularity

The static analysis of programs by parts [36]. This includes separate interprocedural analysis [23].

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 [25]. This provides a unifying view on abstract domain design [49].

There are numerous examples of such abstract domain combinations including the reduced sum, the reduced product and the reduced power [25].

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 [14,5,76], [66], the disjunctive completion [25], [50], the Heyting completion [56], complementation [12], 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 [25], [88,54,55,99].

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 [25]. 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 abstract-interpretation-based 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 [20], octagons [78] or polyhedra are in infinite abstract domains whence required the introduction of new widening-based iteration convergence acceleration methods to become effective.

4.2 Interval analysis

The analysis of the interval in which the values of variables do range [20,21].

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) [78,79,80].

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 [41].

Delay analysis in synchronous programs [61], safety analysis of reactive systems [62], quantitative time properties of synchronous programs, and linear hybrid systems [63] are among the many applications.

4.5 Congruence analysis

The analysis of the congruence invariants satisfied by the values of one [59] or several numerical variables [79].

4.6 Roundoff error analysis

The analysis of the origin of roundoff errors in floating point computations [57,74].

4.7 Symbolic analysis

The analysis of symbolic properties of programs, usually as opposed to numerical program properties e.g. heap reachability analysis [22,23]. 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 model-checking [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 call-by-need by a more efficient call by value [86]. Introduced by Alan Mycroft [87], this analysis was at the origin of the use of abstract interpretation in the functional language community [1,70]. Strictness analysis [8,90] can be embedded in the lattice of comportment analyses [32].

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 [77,42,101,72,73,85,7,11,2], [28].

4.10 Aliasing and pointer analysis

The static analysis of imperative programs must take accesses and side effects through aliases and pointers into account [22]. The profuse literature on pointer analysis is surveyed in [43,65].

4.11 Escape analysis

Escape analysis is a static analysis that determines whether the lifetime of data exceeds its static scope [91,44], [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 [98,97].

4.13 Concurrency analysis

The static analysis of concurrent programs from shared-memory [27] to [a]synchronous communication [26], 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 pi-calculus). This involves the overapproximation of the set of sequences of graphs representing the process allocations and communications at all time instants during execution [103,48].

4.15 Control flow analysis (CFA)

Control flow analysis aims at determining the possible flows of computation in higher-order functional languages [67,100].

4.16 Probabilistic analysis

The static analysis of probabilistic programs [84,82,83], [45].

4.17 WCET analysis

The static determination of the worst-case execution time [46] which involves the analysis of the cache behavior [47], the pipelines, etc.

4.18 Hardware analysis

The static analysis of hardware formal descriptions such as asynchronous circuits [102].

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).

5.2 The Parma Polyhedra Library (PPL)

The Parma Polyhedra Library (PPL) is a user-friendly, fully dynamic, portable, exception-safe, 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 non-strict) with rational coefficients.

5.3 The octagon abstract domain library

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) [80].

6 Abstract-interpretation-based 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.

6.1 Airac5

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.

6.2 aiT WCET Analyzers

Commercial static analyzers from AbsInt Angewandte Informatik to statically compute tight bounds for the worst-case execution time (WCET) of tasks in real-time systems.

6.3 ASTRÉE

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.

6.4 C Global Surveyor

A research prototype static analyzer from the Intelligent Systems Division at the NASA Ames Research Center for finding runtime errors in C programs.

6.5 Fluctuat

A static analyzer from CEA-LIST to study the propagation of rounding errors in floating-point computations of C or assembler programs.

6.6 PolySpace Verifier

A commercial general-purpose static analyzer of PolySpace Technologies for detecting runtime errors in Ada, C, C++, and Java.

6.7 TERMINATOR

A static analyzer from Microsoft Research Cambridge for proving program termination and general liveness properties of C programs.

6.8 TVLA

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:
- The Asian symposium on Programming Languages And Systems APLAS'06,
- The European Symposium on Programming ESOP'07
- The Annual ACM SIGPLAN-SIGACT symposium on Principles Of Programming Languages POPL'07;
Specialized conferences:
- The International Static Analysis Symposium SAS'06;
- The International Conference on Verification, Model Checking and Abstract Interpretation VMCAI'07.

8 Short bibliography

Short bibliography

[1]: S. Abramsky & C. Hankin, editors. - Abstract Interpretation of Declarative Languages. - Ellis Horwood, Chichester, United Kingdom, 1987, Computers and their Applications.
[2]: R. Barbuti, R. Giacobazzi & G. Levi. - A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. ACM Transactions on Programming Languages and Systems, Vol. 15, n 1, January 1993, pp. 133-181.
[3]: J. Berdine, A. Chawdhary, B. Cook, . Distefano & P. O'Hearn. - Variance analyses from invariance analyses. In : Conference Record of the Thirtyfourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Nice, France, 2007. - ACM Press, New York, New York, United States. To appear.
[4]: B. Blanchet. - Escape Analysis for Java^TM. Theory and Practice. ACM Transactions on Programming Languages and Systems, Vol. 25, n 6, November 2003, pp. 713-775.
[5]: F. Bourdoncle. - Abstract Interpretation by Dynamic Partitioning. Journal of Functional Programming, Vol. 2, n 4, 1992, pp. 407-435.
[6]: F. Bourdoncle. - Efficient Chaotic Iteration Strategies with Widenings. In : Proceedings of the International Conference on Formal Methods in Programming and their Applications, edited by D. Bjø rner, M. Broy & I. Pottosin. Akademgorodok, Novosibirsk, Russia, Lecture Notes in Computer Science 735, pp. 128-141. - Springer, Berlin, Germany, 28 June -2 July 1993.
[7]: M. Bruynooghe. - A Practical Framework for the Abstract Interpretation of Logic Programs. Journal of Logic Programming, Vol. 10, n 1,2,3&4, January 1991, pp. 91-124.
[8]: G. Burn, C. Hankin & S. Abramsky. - Strictness Analysis of Higher-Order Functions. Science of Computer Programming, Vol. 7, November 1986, pp. 249-278.
[9]: E. Clarke, O. Grumberg & D. Long. - Model Checking and Abstraction. ACM Transactions on Programming Languages and Systems, Vol. 16, n 5, september 1994, pp. 1512-1542.
[10]: E. Clarke, O. Grumberg & D. Peled. - Model Checking. - MIT Press, Cambridge, Massachusetts, United States, 1999.
[11]: A. Cortesi & G. Filé. - Abstract interpretation of logic programs: an abstract domain for groundness, sharing, freeness and compoundness analysis. In : Proceedings of the ACM Symposium on Partial Evaluation and SemanticsBased Program Manipulation, PEPM '91, edited by P. Hudak & N. Jones, pp. 52-61. - ACM Press, New York, New York, United States, september 1991, Yale U., New Haven, Connecticut, United States, 17-19 June 1991, ACM SIGPLAN Notices 26(9).
[12]: A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi & F. Ranzato. - Complementation in Abstract Interpretation. ACM Transactions on Programming Languages and Systems, Vol. 19, n 1, January 1997, pp. 7-47.
[13]: 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, France, Thèse d'État ès sciences mathématiques, Université scientifique et médicale de Grenoble, 21 March 1978.
[14]: 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. 303-342. - PrenticeHall, Inc., Englewood Cliffs, New Jersey, United States, 1981.
[15]: P. Cousot. - Types as Abstract Interpretations, invited paper. In : Conference Record of the Twentyfourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997. pp. 316-331. - ACM Press, New York, New York, United States.
[16]: P. Cousot. - The Calculational Design of a Generic Abstract Interpreter, invited chapter. In : Calculational System Design, edited by M. Broy & R. Steinbrüggen, pp. 421-505. - NATO Science Series, Series F: Computer and Systems Sciences. IOS Press, Amsterdam, The Netherlands, 1999, Volume 173.
[17]: P. Cousot. - Partial Completeness of Abstract Fixpoint Checking, invited paper. In : Proceedings of the Fourth International Symposium on Abstraction, Reformulation and Approximation, SARA '2000, edited by B. Choueiry & T. Walsh, pp. 1-25. - Springer, Berlin, Germany, 26-29 July 2000, Horseshoe Bay, Texas, United States, Lecture Notes in Artificial Intelligence 1864.
[18]: P. Cousot. - Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Theoretical Computer Science, Vol. 277, n 1-2, 2002, pp. 47-103.
[19]: P. Cousot. - Verification by Abstract Interpretation, invited chapter. In : Proceedings of the International Symposium on Verification - Theory & Practice - Honoring Zohar Manna's 64th Birthday, edited by N. Dershowitz, pp. 243-268. - Taormina, Italy, Lecture Notes in Computer Science 2772, Springer, Berlin, Germany, 29 June - 4 July 2003.
[20]: P. Cousot & R. Cousot. - Static determination of dynamic properties of programs. In : Proceedings of the Second International Symposium on Programming, Paris, France, 1976. pp. 106-130. - Dunod, Paris, France.
[21]: P. Cousot & R. Cousot. - Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of points. In : Conference Record of the Fourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Los Angeles, California, 1977. pp. 238-252. - ACM Press, New York, New York, United States.
[22]: P. Cousot & R. Cousot. - Static determination of dynamic properties of generalized type unions. In : ACM Symposium on Language Design for Reliable Software, Raleigh, North Calorina, ACM SIGPLAN Notices 12(3):77-94, 1977.
[23]: P. Cousot & R. Cousot. - Static determination of dynamic properties of recursive procedures. In : IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., Canada, edited by E. Neuhold. pp. 237-277. - NorthHolland Pub. Co., Amsterdam, The Netherlands, 1977.
[24]: P. Cousot & R. Cousot. - Constructive versions of Tarski's fixed point theorems. Pacific Journal of Mathematics, Vol. 82, n 1, 1979, pp. 43-57.
[25]: P. Cousot & R. Cousot. - Systematic design of program analysis frameworks. In : Conference Record of the Sixth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, 1979. pp. 269-282. - ACM Press, New York, New York, United States.
[26]: P. Cousot & R. Cousot. - Semantic analysis of communicating sequential processes. In : Seventh International Colloquium on Automata, Languages and Programming, edited by J. de Bakker & J. van Leeuwen. Lecture Notes in Computer Science 85, pp. 119-133. - Springer, Berlin, Germany, July 1980.
[27]: 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. 243-271. - Macmillan, New York, New York, United States, 1984.
[28]: P. Cousot & R. Cousot. - Abstract Interpretation and Application to Logic Programs. Journal of Logic Programming, Vol. 13, n 2-3, 1992, pp. 103-179. - (The editor of Journal of Logic Programming has mistakenly published the unreadable galley proof. For a correct version of this paper, see http://www.di.ens.fr/~cousot.).
[29]: P. Cousot & R. Cousot. - Abstract Interpretation Frameworks. Journal of Logic and Computation, Vol. 2, n 4, August 1992, pp. 511-547.
[30]: P. Cousot & R. Cousot. - Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, invited paper. In : Proceedings of the Fourth International Symposium Programming Language Implementation and Logic Programming, PLILP '92, edited by M. Bruynooghe & M. Wirsing. Leuven, Belgium, 26-28 August 1992, Lecture Notes in Computer Science 631, pp. 269-295. - Springer, Berlin, Germany, 1992.
[31]: P. Cousot & R. Cousot. - Inductive Definitions, Semantics and Abstract Interpretation. In : Conference Record of the Ninthteenth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, United States, 1992. pp. 83-94. - ACM Press, New York, New York, United States.
[32]: P. Cousot & R. Cousot. - Higher-Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection and PER Analysis of Functional Languages), invited paper. In : Proceedings of the 1994 International Conference on Computer Languages, Toulouse, France, 16-19 May 1994. pp. 95-112. - IEEE Computer Society Press, Los Alamitos, California, United States.
[33]: P. Cousot & R. Cousot. - Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form, invited paper. In : Proceedings of the Seventh International Conference on Computer Aided Verification, CAV '95, edited by P. Wolper. Liège, Belgium, Lecture Notes in Computer Science 939, pp. 293-308. - Springer, Berlin, Germany, 3-5 July 1995.
[34]: P. Cousot & R. Cousot. - Formal Language, Grammar and SetConstraintBased Program Analysis by Abstract Interpretation. In : Proceedings of the Seventh ACM Conference on Functional Programming Languages and Computer Architecture, La Jolla, California, United States, 25-28 June 1995. pp. 170-181. - ACM Press, New York, New York, United States.
[35]: P. Cousot & R. Cousot. - Temporal Abstract Interpretation. In : Conference Record of the Twentyseventh Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, United States, January 2000. pp. 12-25. - ACM Press, New York, New York, United States.
[36]: P. Cousot & R. Cousot. - Modular Static Program Analysis, invited paper. In : Proceedings of the Eleventh International Conference on Compiler Construction, CC '2002, edited by R. Horspool, Grenoble, France, 6-14 April 2002. pp. 159-178. - Lecture Notes in Computer Science 2304, Springer, Berlin, Germany.
[37]: P. Cousot & R. Cousot. - Systematic Design of Program Transformation Frameworks by Abstract Interrpetation. In : Conference Record of the Twentyninth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Portland, Oregon, United States, January 2002. pp. 178-190. - ACM Press, New York, New York, United States.
[38]: P. Cousot & R. Cousot. - Parsing as Abstract Interpretation of Grammar Semantics. Theoretical Computer Science, Vol. 290, n 1, January 2003, pp. 531-544.
[39]: P. Cousot & R. Cousot. - An Abstract Interpretation-Based Framework for Software Watermarking. In : Conference Record of the Thirtyfirst Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Venice, Italy, 14-16 January 2004. pp. 173-185. - ACM Press, New York, New York, United States.
[40]: P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux & X. Rival. - The ASTRÉE analyser. In : Proceedings of the Fourteenth European Symposium on Programming Languages and Systems, ESOP '2005, Edinburg, Scotland, edited by M. Sagiv, pp. 21-30. - Springer, Berlin, Germany, 2-10 April 2005, Lecture Notes in Computer Science, Vol. 3444.
[41]: P. Cousot & N. Halbwachs. - Automatic discovery of linear restraints among variables of a program. In : Conference Record of the Fifth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Tucson, Arizona, 1978. pp. 84-97. - ACM Press, New York, New York, United States.
[42]: S. Debray & D. Warren. - Automatic mode inferencing for Prolog programs. In : Proceedings of the 1986 International Symposium on Logic Programming, pp. 78-88. - IEEE Computer Society Press, Los Alamitos, California, United States, september 1986, Salt Lake City, Utah.
[43]: A. Deutsch. - Semantic models and abstract interpretation techniques for inductive data structures and pointers, , invited paper. In : Proceedings of the ACM Symposium on Partial Evaluation and SemanticsBased Program Manipulation, PEPM '95, La Jolla, California, 21-23 June 1995. pp. 226-229. - ACM Press, New York, New York, United States.
[44]: A. Deutsch. - On the complexity of escape analysis. In : Conference Record of the Twentyfourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997. pp. 358-371. - ACM Press, New York, New York, United States.
[45]: A. Di Pierro, C. Hankin & H. Wiklicky. - Probabilistic lambda calculus and quantitative program analysis. Journal of Logic and Computation, Vol. 15, n 2, 2005, pp. 159-179.
[46]: C. Ferdinand, R. Heckmann, M. Langenbach, F. Martin, M. Schmidt, H. Theiling, S. Thesing & R. Wilhelm. - Reliable and Precise WCET Determination for a Real-Life Processor. In : Proceedings of the First International Workshop on Embedded Software, EMSOFT '2001, edited by T. Henzinger & C. Kirsch, pp. 469^^d1-485. - Springer, Berlin, Germany, 2001, Lecture Notes in Computer Science, Vol. 2211.
[47]: C. Ferdinand, F. Martin, R. Wilhelm & M. Alt. - Cache behavior prediction by abstract interpretation. Science of Computer Programming, Vol. 35, n 1, 1999, pp. 163-189.
[48]: J. Feret. - Abstract Interpretation-Based Static Analysis of Mobile Ambients. In : Proceedings of the Eight International Symposium on Static Analysis, SAS '01, edited by P. Cousot. Paris, France, Lecture Notes in Computer Science 2126, pp. 413-431. - Springer, Berlin, Germany, 16-18 July 2001.
[49]: G. Filè, R. Giacobazzi & F. Ranzato. - A Unifying View on Abstract Domain Design. ACM Computing Surveys, Vol. 28, n 2, 1996, pp. 333-336.
[50]: G. Filé & F. Ranzato. - The Powerset Operator on Abstract Interpretations. Theoretical Computer Science, Vol. 222, n 1-2, July 1999, pp. 77-111.
[51]: R. Giacobazzi & I. Mastroeni. - Non-Standard Semantics for Program Slicing. Higher-Order and Symbolic Computation, Vol. 16, n 4, 2003, pp. 297-339.
[52]: R. Giacobazzi & I. Mastroeni. - Timed Abstract Non-Interference. In : Proceedings of the Third International Conference on Formal Modelling and Analysis of Timed Systems,FORMATS '05, edited by B. Le Charlier, pp. 289-303. - Springer, Berlin, Germany, 2005, Uppsala, Sweden, 26-28 september 2005, Lecture Notes in Computer Science 3829.
[53]: R. Giacobazzi & E. Quintarelli. - Incompleteness, Counterexamples and Refinements in Abstract Model-Checking. In : Proceedings of the Eight International Symposium on Static Analysis, SAS '01, edited by P. Cousot. Paris, France, Lecture Notes in Computer Science 2126, pp. 356-373. - Springer, Berlin, Germany, 16-18 July 2001.
[54]: R. Giacobazzi & F. Ranzato. - Completeness in Abstract Interpretation: A Domain Perspective. In : Proceedings of the Sixth International Conference on Algebraic Methodology and Software Technology, AMAST '97, Sydney, Australia, edited by M. Johnson. Lecture Notes in Computer Science, Vol. 1349, pp. 231-245. - Springer, Berlin, Germany, 13-18 December 1997.
[55]: R. Giacobazzi, F. Ranzato & F. Scozzari. - Making Abstract Interpretations Complete. Journal of the Association for Computing Machinary, Vol. 47, n 2, 2000, pp. 361-416.
[56]: R. Giacobazzi & F. Scozzari. - A logical model for relational abstract domains. ACM Transactions on Programming Languages and Systems, Vol. 20, n 5, 1998, pp. 1067-1109.
[57]: É. Goubault, M. Martel & S. Putot. - Asserting the precision of floating-point computations: a simple abstract interrpeter. In : Proceedings of the Eleventh European Symposium on Programming Languages and Systems, ESOP '2002, edited by D. Le Métayer, pp. 209-212. - Springer, Berlin, Germany, 8-12 April 2002, Grenoble, France, Lecture Notes in Computer Science 2305.
[58]: S. Graf & H. Saïdi. - Verifying Invariants Using Theorem Proving. In : Proceedings of the Eight International Conference on Computer Aided Verification, CAV '97, edited by R. Alur & T. Henzinger. New Brunswick, New Jersey, United States, Lecture Notes in Computer Science 1102, pp. 196-207. - Springer, Berlin, Germany, July 31 - August 3 1996.
[59]: P. Granger. - Static Analysis of Arithmetical Congruences. Int. J. Comput. Math., Vol. 30, 1989, pp. 165-190.
[60]: P. Granger. - Static Analysis of Linear Congruence Equalities among Variables of a Program. In : Proceedings of the International Joint Conference on Theory and Practice of Software Development, TAPSOFT '91, Volume 1 (CAAP '91), edited by S. Abramsky & T. Maibaum. Brighton, Great Britain, Lecture Notes in Computer Science 493, pp. 169-192. - Springer, Berlin, Germany, 1991.
[61]: N. Halbwachs. - Delay Analysis in Synchronous Programs. In : Proceedings of the Fifth International Conference on Computer Aided Verification, CAV '93, edited by C. Courcoubatis. Elounda, Greece, Lecture Notes in Computer Science 697, pp. 333-346. - Springer, Berlin, Germany, 28 June -1 July 1993.
[62]: N. Halbwachs. - About Synchronous Programming and Abstract Interpretation. In : Proceedings of the First International Symposium on Static Analysis, SAS '94, edited by B. Le Charlier, pp. 179-192. - Springer, Berlin, Germany, 1994, Namur, Belgium, 20-22 september 1994, Lecture Notes in Computer Science 864.
[63]: N. Halbwachs, Y. Proy & P. Roumanoff. - Verification of real-time systems using linear relation analysis. Formal Methods in System Design, Vol. 11, n 2, August 1997, pp. 157-185.
[64]: M. Hecht. - Flow Analysis of Computer Programs. - NorthHolland/Elsevier Science Publishers B.V., Amsterdam, The Netherlands, 1977.
[65]: M. Hind. - Pointer Analysis: Haven't We Solved This Problem Yet? In : 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE '01, Snowbird, Utah, United States, 2001.
[66]: B. Jeannet, N. Halbwachs & P. Raymond. - Dynamic Partitioning in Analyses of Numerical Properties. In : Proceedings of the Sixth International Symposium on Static Analysis, SAS '99, edited by A. Cortesi,name G. Filé, pp. 18-38. - Springer, Berlin, Germany, 1999, Venice, Italy, 22-24 september 1999, Lecture Notes in Computer Science 1694.
[67]: N. Jones. - Flow Analysis of Lambda Expressions (Preliminary Version). In : Eight International Colloquium on Automata, Languages and Programming, edited by S. Even & O. Kariv. Lecture Notes in Computer Science 115, pp. 114-128. - Springer, Berlin, Germany, July 1981.
[68]: N. Jones. - Combining Abstract Interpretation and Partial Evaluation (Brief Overview). In : Proceedings of the Fourth International Symposium on Static Analysis, SAS '97, edited by P. Van Hentenryck, pp. 396-405. - Springer, Berlin, Germany, 1997, Paris, France, 8-10 september 1997, Lecture Notes in Computer Science 1302.
[69]: N. Jones, C. Gomard & P. Sestoft. - Partial Evaluation and Automatic Program Generation. - PrenticeHall, Inc., Englewood Cliffs, New Jersey, United States, June 1993, International Series in Computer Science.
[70]: N. Jones & F. Nielson. - Abstract interpretation: a semantics-based tool for program analysis. In : Semantic Modelling, edited by S. Abramsky, D. Gabbay & T. Maibaum, Chapter 5, pp. 527-636. - Clarendon Press, Oxford, United Kingdom, 1995, Handbook of Logic in Computer Science, Vol. 4.
[71]: N. Jones & M. Rosendahl. - Higher-Order Minimal Function Graphs. Journal of Functional and Logic Programming, Vol. 1997, n 2, February 1997.
[72]: H. Mannila & E. Ukkonen. - Flow analysis of Prolog programs. In : Proceedings of the 1987 International Symposium on Logic Programming. San Francisco, California, pp. 205-214. - IEEE Computer Society Press, Los Alamitos, California, United States, 31 August - 4september 1987.
[73]: K. Marriott & H. Søndergaard. - Bottom-Up Abstract Interpretation of Logic Programs. In : Proceedings of the Fifth International Conference and Symposium on Logic Programming, Volume 1, edited by R. Kowalski & K. Bowen. Seattle, Washington, United States, pp. 733-748. - MIT Press, Cambridge, Massachusetts, United States, 15-19 August 1988.
[74]: M. Martel. - An Overview of Semantics for the Validation of Numerical Programs. In : Proceedings of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2005), edited by R. Cousot, Paris, France, 17-19 January 2005. pp. 59-77. - Lecture Notes in Computer Science 3385, Springer, Berlin, Germany.
[75]: L. Mauborgne. - Tree Schemata and Fair Termination. In : Proceedings of the Seventh International Symposium on Static Analysis, SAS '2000, edited by J. Palsberg, pp. 302-321. - Springer, Berlin, Germany, 29 June - 1 July 2000, Santa Barbara, California, United States, Lecture Notes in Computer Science 1824.
[76]: L. Mauborgne & X. Rival. - Trace Partitioning in Abstract Interpretation Based Static Analyzer. In : Proceedings of the Fourteenth European Symposium on Programming Languages and Systems, ESOP '2005, Edinburg, Scotland, edited by M. Sagiv, pp. 5-20. - Springer, Berlin, Germany, April 2^^d1-10, 2005, Lecture Notes in Computer Science, Vol. 3444.
[77]: C. Mellish. - Abstract Interpretation of Prolog Programs. In : Third International Conference on Logic Programming, ICLP '86, edited by E. Shapiro, pp. 463-474. - Springer, Berlin, Germany, 14-18 July 1986, London, Great Britain, Lecture Notes in Computer Science 225.
[78]: A. Miné. - A New Numerical Abstract Domain Based on DifferenceBound Matrices. In : Proceedings of the Second Symposium PADO '2001, Programs as Data Objects, edited by . Danvy & A. Filinski. Å rhus, Denmark, 21-23 May 2001, Lecture Notes in Computer Science 2053, pp. 155-172. - Springer, Berlin, Germany, 2001.
[79]: A. Miné. - A Few Graph-Based Relational Numerical Abstract Domains. In : Proceedings of the Ninth International Symposium on Static Analysis, SAS '02, edited by M. Hermenegildo,name G. Puebla. Lecture Notes in Computer Science, Vol. 2477, pp. 117-132. - Springer, Berlin, Germany, 2002.
[80]: A. Miné. - The Octagon Abstract Domain. Higher-Order and Symbolic Computation, Vol. 19, 2006, pp. 31-100.
[81]: D. Monniaux. - An Abstract Analysis of the Probabilistic Termination of Programs. In : Proceedings of the Eight International Symposium on Static Analysis, SAS '01, edited by P. Cousot. Paris, France, Lecture Notes in Computer Science 2126, pp. 111-127. - Springer, Berlin, Germany, 16-18 July 2001.
[82]: D. Monniaux. - An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs (extended abstract). In : Conference Record of the Twentyeight Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, London, Great Britain, January 2001. pp. 93-101. - ACM Press, New York, New York, United States.
[83]: D. Monniaux. - Backwards abstract interpretation of probabilistic programs. In : Proceedings of the Tenth European Symposium on Programming Languages and Systems, ESOP '2001, edited by D. Sands. Genova, Italy, 2-6 April 2001, Lecture Notes in Computer Science 2028, pp. 367-382. - Springer, Berlin, Germany, 2001.
[84]: D. Monniaux. - Abstract interpretation of probabilistic semantics. In : Proceedings of the Seventh International Symposium on Static Analysis, SAS '2000, edited by J. Palsberg, pp. 322-339. - Springer, Berlin, Germany, 29 June - 1 July 2000, Santa Barbara, California, United States, Lecture Notes in Computer Science 1824.
[85]: K. Muthukumar & M. Hermenegildo. - Determination of Variable Dependence Information through Abstract Interpretation. In : Logic Programming, Proceedings of the 1989 North American Conference , NACLP 1989, Volume 1, edited by E. Lusk & R. Overbeek. Cleaveland, Ohio, United States, pp. 166-185. - MIT Press, Cambridge, Massachusetts, United States, 16-20 October 1989.
[86]: A. Mycroft. - The theory and practice of transforming call-by-need into call-by-value. In : Proceedings of the Fourth International Symposium on Programming, edited by B. Robinet, pp. 270-281. - Springer, Berlin, Germany, 1980, Paris, France, 22-24 April 1980, Lecture Notes in Computer Science 83.
[87]: A. Mycroft. - Abstract Interpretation and Optimising Transformations for Applicative Programs. - Edinburg, Scotland, Ph.D. Dissertation, CST-15-81, Department of Computer Science, University of Edinburgh, December 1981.
[88]: A. Mycroft. - Completeness and predicate-based abstract interpretation. In : Proceedings of the ACM Symposium on Partial Evaluation and SemanticsBased Program Manipulation, PEPM '93. Copenhagen, Denmark, 14-16 June 1993, pp. 80-87. - ACM Press, New York, New York, United States, 1993.
[89]: 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. 156-171. - Springer, Berlin, Germany, 1986, Copenhagen, Denmark, 17-19 October 1985, Lecture Notes in Computer Science 215.
[90]: F. Nielson. - Strictness Analysis and Denotational Abstract Interpretation. In : Conference Record of the Fourteenth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Munchen, Germany, 1987. pp. 120-131. - ACM Press, New York, New York, United States.
[91]: Y. G. Park & B. Goldberg. - Escape analysis on lists. In : Proceedings of the ACM SIGPLAN '92 Conference on Programming Language Design and Implementation (PLDI). ACM SIGPLAN Notices 31(5), San Francisco, California, United States, 21-24, May 1992. pp. 116-127. - ACM Press, New York, New York, United States.
[92]: B. Pierce. - Types and Programming Languages. - MIT Press, Cambridge, Massachusetts, United States, 2002.
[93]: M. D. Preda, M. Christodorescu, S. Jha & S. Debray. - A Semantics-Based Approach to Malware Detection. In : Conference Record of the Thirtyfourth Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Nice, France, 2007. - ACM Press, New York, New York, United States. To appear.
[94]: M. D. Preda & R. Giacobazzi. - Control Code Obfuscation by Abstract Interpretation. In : Proceedings of the Third IEEEInternational Conference on Software Engineering and Formal Methods, SEFM '05, Koblenz, Germany, 2005. - IEEE Computer Society Press, Los Alamitos, California, United States.
[95]: F. Ranzato. - On the Completeness of Model Checking. In : Proceedings of the Tenth European Symposium on Programming Languages and Systems, ESOP '2001, edited by D. Sands. Genova, Italy, 2-6 April 2001, Lecture Notes in Computer Science 2028, pp. 137-154. - Springer, Berlin, Germany, 2001.
[96]: F. Ranzato & F. Tapparo. - Strong Preservation of Temporal Fixpoint-Based Operators by Abstract Interpretation. In : Proceedings of the Seventh International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2006), edited by A. Emerson & K. Namjoshi, Charleston, South Carolina, United States, 8-10 January 2006. pp. 332-347. - Lecture Notes in Computer Science 3855 , Springer, Berlin, Germany.
[97]: N. Rinetzky, J. Bauer, T. Reps, S. Sagiv & R. Wilhelm. - A semantics for procedure local heaps and its abstractions. In : Conference Record of the Thirtysecond Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Long Beach, California, United States, 2005. pp. 296-309. - ACM Press, New York, New York, United States.
[98]: M. Sagiv, T. Reps & R. Wilhelm. - Shape Analysis. In : Proceedings of the International Conference on Compiler Construction, CC '2000, Lecture Notes in Computer Science 1781, edited by D. A. Watt, Berlin, Germany, 25 March - 2 April 2000. pp. 1-17. - Springer, Berlin, Germany.
[99]: D. Schmidt. - Comparing completeness properties of static analyses and their logics. In : Proceedings of the Fourth Asian Symposium on Programming Languages and Systems, APLAS '2006, edited by N. Kobayashi, Sydney, Australia, 3-5 November 2006. pp. 135-138. - Lecture Notes in Computer Science 4279, Springer, Berlin, Germany.
[100]: O. Shivers. - Higher-order control-flow analysis in retrospect: lessons learned, lessons abandoned. ACM SIGPLAN Notices, Vol. 39, n 4, 2004, pp. 257-269.
[101]: H. Søndergaard. - An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction. In : Proceedings of the European Symposium on Programming Languages and Systems, ESOP '86, edited by B. Robinet,name R. Wilhelm, pp. 327-338. - Springer, Berlin, Germany, 1986, Saarbrücken, Germany, 17-19 March 1986, Lecture Notes in Computer Science 213.
[102]: S. Thompson & A. Mycroft. - Abstract Interpretation of Combinational Asynchronous Circuits. In : Proceedings of the Eleventh International Symposium on Static Analysis, SAS '04, edited by R. Giacobazzi. Verona, Italy, Lecture Notes in Computer Science 3148, pp. 181-196. - Springer, Berlin, Germany, 26-28 August 2004.
[103]: A. Venet. - Automatic Determination of Communication Topologies in Mobile Systems. In : Proceedings of the Fifth International Symposium on Static Analysis, SAS '98, edited by G. Levi, pp. 152-167. - Springer, Berlin, Germany, 1998, Pisa, Italy, 14-16 september 1998, Lecture Notes in Computer Science 1503.

PDF version.

This document is hopefully sound, may be too abstract and necessarily incomplete. Amendments are welcomed at Patrick.Cousot@ens.fr.

Footnotes:

¹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 counter-intuitive.