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.
Patrick Cousot received the Doctor Engineer degree in Computer Science and the Doctor ès Sciences degree in Mathematics from the University Joseph Fourier of Grenoble, France. Patrick Cousot is currently Professor of Computer Science at the Courant Institute of Mathematical Sciences, New York University, USA and the École Normale Supérieure, Paris, France. Before he was Professor at the École Polytechnique and the University of Metz and a Research Scientist at the French National Center for Scientific Research at the University Joseph Fourier of Grenoble, France.
Patrick Cousot is the inventor, with Radhia Cousot, of Abstract Interpretation. Patrick Cousot was awarded the Silver Medal of the CNRS (1999), a honorary doctorate from the Fakultät Mathematik und Informatik of the Universität des Saarlandes (2001), the Grand Prix of Computer Science and its Applications of the EADS Corporate Research Foundation attributed by the French Academy of Sciences (2006) and a Humboldt Research Award (2008). He is Member of the Academia Europæa (since 2006).
Catherine Copetas, copetas [atsymbol] cs.cmu.edu