Abstract:
Abstract interpretation is a theory of abstraction and constructive approximation of the mathematical structures used in the formal description of complex or infinite systems and the inference or verification of their combinatorial or undecidable properties. Developed in the late seventies with Radhia Cousot, it has been since then applied to many aspects of computer science (such as static analysis and verification, contract inference, type inference, termination inference, model-checking, abstraction refinement, program transformation (including watermarking), combination of decision procedures, security, malware detection, database queries, etc.) and more recently, to system biology.
The talk will consist in an introduction to the basic notions of abstract interpretation and the induced methodology for the systematic development of sound abstract interpretation-based tools. Examples of abstractions will be provided, from semantics to typing, grammars to safety, reachability to potential/definite termination, numerical to protein-protein abstractions, as well as applications (including in industrial use) to software, hardware and system biology.
\bibitem{Cousot-CMU-GOML-2012}
Patrick Cousot (joint work with Radhia Cousot).
\newblock Abstract Interpretation: Principles and Applications.
\newblock Gaschnig/Oakley Memorial Lecture (SCS Distinguished Lecture Series),
School of Computer Science, Carnegie Mellon University, April 12, 2012.
@inproceedings{Cousot-CMU-GOML-2012,
author = "Patrick Cousot (joint work with Radhia Cousot)",
title = "Abstract Interpretation: Principles and Applications.",
booktitle = "Gaschnig/Oakley Memorial Lecture (SCS Distinguished Lecture Series)",
series = "School of Computer Science, Carnegie Mellon University",
publisher = "Springer-Verlag",
month = "12 April",
year = 2012,
}