Patrick COUSOT    Professor of Computer Science    Courant Institute of Mathematical Sciences    New York University

Abstract Interpretation, introduced in the seventies by Patrick Cousot and Radhia Cousot, is a theory of sound abstraction and approximation of complex mathematical structures, in particular those involved in the description of computer and biological systems.

The essential idea extensively developed and deepened in Abstract Interpretation is that any manual or automatic reasoning on complex systems requires abstractions of the semantics defining their behavior to intrinsic, more abstract, properties. Moreover, full automation must involve sound approximations of these properties. The theory guaranties soundness so that all claims made in the abstract are always valid in the concrete, although sometimes incomplete, due to undecidability.

A distinctive and very powerful characteristic of Abstract Interpretation is the use of a composition of infinitary abstractions to infer complex properties (using widenings and narrowings to abstract induction and co-induction in fixpoint computations). A consequence is that Abstract Interpretation is provably strictly more powerful than checking finite models of computations.

Abstract Interpretation provides a unifying algebraic theory of syntax, semantics and formal methods. In practice, it offers the rigorous basis for the systematic derivation of sound methods and algorithms for approximating undecidable or highly complex problems in various areas of computer science (such as syntax, semantics, specification and design, functional and safety verification and proof of hardware and software, security verification and proof (e.g. confidentiality, integrity and availability), model-checking, sound static analysis, typing, invariant inference, termination verification and inference, compilation, program transformation and optimization, parallelization, program refactoring, software obfuscation and watermarking, malware detection, data base coherence verification and query optimization, etc.).

Abstract Interpretation does scale up to automatically verify very large systems without requiring handmade simplified models or human interaction. The current main industrial applications of Abstract Interpretation are automatic tools for the precise verification of safety and security of complex hardware and software computer systems including programs of several millions lines of code as found in the avionics, automotive, banking, medical, nuclear and space industries. Its latest emerging application is the analysis of complex molecular networks in cellular signaling systems.