Most of these problems arise from the use of inadequate abstractions (in the sense of the theory of Abstract Interpretation). By choosing appropriate infinitary, domain-aware, parametric and modular abstractions, one can design and implement automatic, sound, efficient and precise verifiers of complex properties for example of embedded, real-time, synchronous, safety super-critical, control-command software.

     The seminar includes a few elements of abstract interpretation theory, a description of an application to the ASTRÉE static analyzer (http://www.astree.ens.fr) including the abstractions which have been used to prove fully automatically the absence of any run-time error in the primary flight control software of the Airbus A340 fly-by-wire system, a world première.

\bibitem{CousotCousot-NYU04}
P{.} Cousot and R{.} Cousot.
\newblock Verification of Safety-Critical Control-Command Sofware by
          Abstract Interpretation.
\newblock Seminar, Computer Science Department, Courant Institute of
          Mathematical Sciences, New York University, New York, NY, USA. 13
          May 2004.

@conference{CousotCousot-NYU04,
   author =    {P{.} Cousot and R{.} Cousot},
   title =     {Verification of Safety-Critical Control-Command Sofware by 
                Abstract Interpretation},
   booktitle = {Seminar},
   address =   {Computer Science Department, Courant Institute of
                Mathematical Sciences, New York University, New York, NY,
                USA},
   month =     {13 May},
   year =      2004,
}