Joint Colloquium Distinguished Lecture Series

Static Verification of Critical Embedded Software By Abstract Interpretation.

Wednesday, November 9th HP Auditorium, Soda Hall 4:00 Patrick Cousot Professor of Computer Science Ecole Normale Supérieure, Paris

Abstract:

This talk briefly reviews abstract interpretation and its main applications. It then presents a practical application of abstract interpretation to the verification of safety critical embedded control-command software by the ASTR\'EE static analyzer. It has been applied with success to the verification of absence of runtime errors in the control part of the primary flight control software of fly-by-wire systems of commercial planes. The state space of such huge programs (hundreds of thousands of lines) is so large that it cannot be explored explicitly by model-checking nor reasonably covered by testing. A (computer-aided) formal proof would be humanely insurmountable and economically very costly. The key to the verification by static analysis is the appropriate experimental choice of abstractions which can be tuned to yield no false alarm, certainly a world premi\`ere for a program of that size (see the ASTR\'EE project, http://www.astree.ens.fr/). We will conclude by grand challenges for static program/specification analysis the next 5 to 10 years.

Biography:

Patrick Cousot is Professor of Computer Science at \'Ecole Normale Sup\'erieure, Paris, France, where he chairs the department's educational programme, and leads the Abstract Interpretation and Semantics research group. Professor Cousot is a renowned authority on static analysis and semantics, and the inventor of the static program analysis framework known as "abstract interpretation".

Return to EECS Joint Colloquium