about this paper

presentation award abstract bibitem


paper editor link
Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, and Xavier Rival.
Static Analysis and Verification of Aerospace Software by Abstract Interpretation.
AIAA Paper 2010-3385 in AIAA Infotech@Aerospace 2010, Atlanta, Georgia. American Institute of Aeronautics and Astronautics, 20—22 April 2010.

This paper has been selected by the AIAA Intelligent Systems Technical Committee as the Best Paper from the AIAA 2010 Infotech@Aerospace Conference.

Abstract: We discuss the principles of static analysis by abstract interpretation and report on the automatic verification of the absence of runtime errors in large embedded aerospace software by static analysis based on abstract interpretation. The first industrial applications concerned synchronous control/command software in open loop. Recent advances consider imperfectly synchronous, parallel programs, and target code validation as well. Future research directions on abstract interpretation are also discussed in the context of aerospace software.

   author =    {J.~Bertrane and P.~ Cousot and R.~ Cousot and J.~ Feret and L.~ Mauborgne 
                and A.~ Miné and X.~ Rival},
   title =     {Static Analysis and Verification of Aerospace Software by Abstract Interpretation},
   booktitle = {AIAA Infotech@Aerospace 2010},
   address =   {Atlanta, Georgia},
   publisher = {American Institute of Aeronautics and Astronautics},
   month =     {20--22 April},
   year =      2010,