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 talk 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.

• PostScript: 1/1 .ps.gz, 2/1 .ps.gz, 4/1 .ps.gz for viewing with GhostScript and GhostView or (color) printing;
• PDF: 1/1 .pdf, 2/1 .pdf, 4/1 .pdf to be used with Acrobat Reader.

\bibitem{Cousot-PROLE04talk}
P{.} Cousot.
\newblock Software Verification by Abstract Interpretation: Current Trends 
          and Perspectives.
\newblock Invited Talk, IV Jornadas de Programaci{\'o}n y Lenguajes, M{\'a}laga, 
          Spain. 11--12 November 2004.

@conference{Cousot-PROLE04talk,
   author =    {P{.} Cousot},
   title =     {Software Verification by Abstract Interpretation: Current Trends 
                and Perspectives},
   booktitle = {Invited Talk},
   address =   {IV Jornadas de Programaci{\'o}n y Lenguajes, M{\'a}laga, 
                Spain},
   month =     {11--12 November},
   year =      2004,
}