[PRL] FW: TALK:Thursday 6-16-05 The ASTREE static analyzer

[Paul A. Steckler]

Mmmm, I can't attend.

-- Paul

---- original message ----

The ASTREE static analyzer
Speaker: Patrick Cousot
Speaker Affiliation: Ecole Normale Superieure, Paris, France
Host: Daniel Jackson
Host Affiliation: EECS/CSAIL

Date: 6-16-2005
Time: 2:00 PM - 3:30 PM
Location: Stata Center, 32-D463 (Star)

The ASTREE static analyzer
Patrick Cousot
Ecole Normale Superieure, Paris, France



The 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 ASTREE 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 premiere for a
program of that size (see the ASTREE project,
http://www.astree.ens.fr/).  We will conclude by grand challenges for
static program/specification analysis the next 5 to 10 years.

Patrick Cousot is Professor of Computer Science at Ecole Normale
Superieure, Paris, France, where he chairs the department's educational
programme, and leads the Abstract Interpretation and Semantics research
group. He has been the J.C. Hunsaker visiting professor at the MIT
Aero-Astro department this past term.  Professor Cousot is a renowned
authority on static analysis and semantics, and the inventor of the
analysis framework known as "abstract interpretation".

Host: Daniel Jackson, EECS/CSAIL

Relevant URL(S): 
For more information please contact: Maria Rebelo, 3-5895,
mr at csail.mit.edu