Formal methods for informal developpers: A case-study driven by the French defense agency (DGA)

Static analysis and formal methods are slowly finding their way in development processes. However, applying such technology requires methodologies and common understanding, which is not always widely spread. In this paper, we´ll describe how the French defense agency DGA is planning to audit such software in the context of military applications written in Ada.