Seminar/2017-09-27
From LRDE
Mercredi 27 septembre 2017, 11h-12h, Salle L0 du LRDE
Frama-C, une plateforme collaborative et extensible pour l'analyse de code C
Julien Signoles, CEA LIST, Laboratoire de Sûreté des Logiciels (LSL)
Frama-C est une plateforme d'analyse de code C visant à vérifier des programmes C de taille industrielle. Elle fournit à ses utilisateurs une collection de greffons effectuant notamment des analyses statiques par interprétation abstraite et des méthodes déductives ou encore permettant des vérifications à l'exécution. La plateforme permet également de faire coopérer les analyses grâce au partage d'un noyau et d'un langage de spécification communs.
Cet exposé présente une vue générale de la plateforme, de ses principaux
analyseurs et de quelques applications industrielles. Il se concentre sur le
langage de spécification ACSL et sur différentes façons de vérifier des
spécifications ACSL avec des analyses statiques ou dynamiques.
Julien Signoles a obtenu un doctorat en informatique de l'Université
Paris 11 en 2006. Il devint ensuite ingénieur-chercheur au CEA LIST
en 2007. Au sein du Laboratoire de Sûreté des Logiciels (LSL), il est l'un des
développeurs principaux de Frama-C. Ses recherches se concentrent aujourd'hui
sur la vérification à l'exécution (runtime verification) et ses différentes
applications pour améliorer la sûreté et la sécurité des logiciels critiques.
orateur : http://julien.signoles.free.fr "orateur " has not been listed as valid URI scheme., projet : http://frama-c.com "projet " has not been listed as valid URI scheme.