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.
\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,
}