Publications by themes of Patrick COUSOT


Introductions to abstract interpretation

These starters are introductions to abstract interpretation theory and practice.


Foundations of abstract interpretation

Abstract interpretation is a theory of discrete approximation of properties of the semantics of computer systems mainly applied to their static analysis and verification.


Galois connections

Galois connections are used in abstract interpretation to formalize the notion of best abstraction, transformers, etc.


Widening/narrowing

Effective iterative fixpoint approximation computation by convergence acceleration.


Numerical abstract domains

An abstract domain encapsulates the basic abstract properties and transformers for analyzing program properties. Numerical abstract domains are related to properties of integer/float values computed by programs.


Symbolic abstract domains

Symbolic abstract domains are related to properties of symbolic values computed by programs (arrays, heap, pointers, etc).


(Higher-order) procedure, function and module abstract interpretation

The abstract interpretation of properties of recursive (higher-order) procedures, functions, modules, etc.


Resolution-based abstract interpretation

The abstract interpretation of properties of resolution-based computing systems such as Prolog.


Concurrency abstract interpretation

The abstract interpretation of properties of concurrent, parallel, communicating, cooperating, and distributed computer systems.


Syntax and abstract interpretation

The approximation idea formalized by abstract interpretation has many applications in the syntactic aspects of computer science (as described by formal languages, grammars, polynomial systems, etc.).


Semantics and abstract interpretation

Semantics are approximate descriptions of the program runtime behavior and therefore can be organized in a hierarchy by abstract interpretation.


Verification

Verification proves that an abstract semantics of computer systems satisfies an abstract specification.


Program proving and abstract interpretation

Program proof methods are abstract interpretations of the program semantics.


Typing and abstract interpretation

Type specification and inference is a static approximation of dynamic typing and as such can be understood as an abstract interpretation of the program semantics.


Static program analysis and abstract interpretation

The primary application of abstract interpretation is to static program analysis undrstood as a static approximation of the dynmic properties of programs, as formalized by a collecting semantics. A priori approximations are formalized by Galois connections and numerous variants while on the fly approximations are formalized by acceleration of the convergence of fixpoint computations by widening/narrowing.


Model checking and abstract interpretation

Model checking is an abstract interpretation. Abstract interpretation can also be used to derive abstract models from concrete models (such as semantics).


Abstraction refinement

Temporal verification of finite systems by refinement of an abstraction.


Semi-definite programming and abstract interpretation

Experience is using semi-definite programming to verify programs.


Control/command and abstract interpretation


Program testing and abstract interpretation

Program testing can be generalized at any level of abstraction by abstract interpretation of the program semantics.


Program transformation and abstract interpretation

Program transformation is a syntactic approximation of a transformation of the semantics of the original program which can be formalized by abstract interpretation.


Steganography and abstract interpretation

Program watermarking by abstract interpretation of its semantics (the mark of a program is an abstraction of its semantics).


Formal methods and abstract interpretation

Formal methods involve reasoning on approximations of the behavior of computer systems as formalized by abstract interpretation.


Pedagogical abstract interpretation-based software

Pedagogical software illustrating the design of static analyzers and verifiers by abstract interpretation.


Design of static analyzers

The design of precise static analyzers that scale-up in industrial context.


Industrialized abstract interpretation-based software

Commercially available software to prove the absence of runtime errors in safety/mission-critical synchronous real-time control/command embedded software and experiences of use in an industrila context.


Mathematics

Mathematical results developped in the context of abstract interpretation theory.


Last modified : Saturday, 02-Jan-2010 10:48:04 CET