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.
An alternative is to use static analysis where an abstraction of the semantics of the programs is automatically computed which leaves out all information about reachable states which is not strictly necessary for the proof. Of course if the abstraction is too precise, the computation cost are too high (resourse exhaustion) and if it is too rough, nothing can be proved (false alarm). Although the best abstraction does exist, it is not computable, and so, must be found experimentally.
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 premi\`ere for a program of that size (see the ASTRÉE project, http://www.astree.ens.fr/). We will conclude by grand challenges for static program/specification analysis the next 5 to 10 years.
\bibitem{Cousot-CAM-20-10-04}
P{.} Cousot.
\newblock Automatic verification of avionic synchronous safety critical
embedded software.
\newblock Wednesday Seminar, The Computer Laboratory, University of
Cambridge, Cambridge, UK. 20 October 2004.
@conference{Cousot-CAM-20-10-04,
author = {P{.} Cousot},
title = {Automatic verification of avionic synchronous safety
critical embedded software},
booktitle = {Wednesday Seminar},
address = {The Computer Laboratory, University of Cambridge,
Cambridge, UK},
month = {20 October},
year = 2004,
}