Publications by research themes of Patrick COUSOT


Introductions to abstract interpretation

These starters are introductions to abstract interpretation theory and practice.


Surveys and position papers on abstract interpretation

Attempts to give an overview of the abstract interpretation research field, with numerous references.


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 and their duals

Effective iterative fixpoint approximation computation by convergence acceleration using extrapolation and interpolation operators.


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


Logical abstract domains

The abstract interpretation of properties encoded as logical formulae over some decidable theory.


Combination of abstractions, abstract domain functors

The design of abstract interpreters by combination of abstract domains


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


Termination abstract interpretation

Termination and eventuality proofs are abstractions of the programs semantics and can therefore be automatized by induction on the structure of computations by fixpoint approximation.


Probabilistic abstract interpretation

Abstract interpretation of probabilistic semantics of computer systems.


Syntax, parsing, 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 and abstract interpretation

Verification proves that an abstract semantics of computer systems satisfies an abstract specification, as formalized by abstract interpretation.


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.


Code contracts static verification and inference

Code contracts are program specifications inlined in the code source (pre/post-conditions, class invariants, ...) that can be checked by abstract interpretation or even infered from the language and programmer assertions.


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. This includes compiler optimization, partial evaluation, refactoring, etc.


Steganography and abstract interpretation

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


Security and abstract interpretation

Software security is based on a deep understanding of the behavior of computer systems as formalized by abstract interpretation.


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.


Early work on the syntax, operational semantics and implementation of programming languages