Re: ASTREE

On Thu, 26 May 2005, Mitch Wand announced:

> ...
>
> We will provide an intuition for the underlying theory, that of
> abstract interpretation, and then report on an application to the
> proof of absence of runtime errors in the electric flight control
> system of commercial planes.  In this project the abstraction has been
> tuned manually to get no false alarm, whence a correctness proof,
> certainly a world premiere for a program of that size (see the
> ASTREE project, http://www.astree.ens.fr/).

It should be noted they analyze C programs(!):

"Industrial Applications of ASTREE

"The development of ASTREE started from scratch in Nov. 2001. Two years
later, the main applications have been the static analysis of synchronous,
time-triggered, real-time, safety critical, embedded software written or
automatically generated in the C programming language. ASTREE has achieved
the following two unprecedented results:

    * "In Nov. 2003, ASTREE was able to prove completely
automatically the absence of any RTE in the primary flight control
software of the Airbus A340 fly-by-wire system, a program of 132,000 lines
of C analyzed in 1h20 on a 2.8 GHz 32-bit PC using 300 Mb of memory (and
50mn on a 64-bit AMD Athlon(tm) 64 using 580 Mb of memory).

    * "Since Jan. 2004, ASTREE is being extended to analyze the
electric flight control codes in development and test for the A380 series.
The operational application is planned by Airbus France by the end of
2004.