Title: Static Analysis and Verification of Synchronous Embedded Code by Abstract Interpretation

Patrick Cousot


Abstract

After a short formal introduction to abstract interpretation and its main 
application to static analysis, we discuss the unique features of ASTRE'E 
(http://www.astree.ens.fr), a static analyser for the verification of absence of 
runtime errors in mission/safety-critical synchronous control/command programs. 
The talk is followed by a short demo.