J'ai fait hier soir une présentation Gulliver sur Frama-C, un framework qui permet notamment de faire de l'analyse et de la preuve sur du code C. Les transparents et exemples sont disponibles (réutilisez les, c'est du Libre !).

Suite à l'annonce de ces transparents sur la liste frama-c-discuss, une très intéressante discussion a démarré sur l'utilisation concrète de Frama-C sur des codes industriels et les avantages respectifs de l'analyse de valeur et la preuve. Je recommande de lire notamment les points de vue de quelqu'un d'Atos Origin (avec des remarques encore plus précises sur la manière de faire ces analyses) et de quelqu'un de chez Dassault Aviation.

Apparemment, Frama-C est utilisé sur du code industriel et il donne des résultats. Intéressant !