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.