Cet ouvrage présente des exemples concrets d'utilisations

industrielles des techniques formelles. Ces techniques réalisent

des modèles de spécifications et/ou de conception et servent

également à l'analyse statique de code, à la démonstration du

respect de propriété, à la bonne gestion des calculs sur les

flottants, etc.

Les standards des différents domaines prennent en compte la

mise en oeuvre des méthodes formelles comme moyen de

construire un logiciel critique de sécurité.

Les exemples industriels de mise en oeuvre des techniques

formelles basées sur l'analyse statique, comme l'interprétation

abstraite avec des exemples d'utilisation des outils Astrée,

Caveat, CodePeer, Framac ou Polyspace sont détaillés.