L'Agenda du Libre

L'association Gulliver organise une présentation de Frama-C, lundi 31 janvier 2011 à partir de 20h, à la MCE (Maison de la Consommation et de l'Environnement, 48 bd Magenta à Rennes), salle de réunion dans les algéco (contourner la MCE par la droite, au fond de la cours).

Le framework Frama-C est un framework libre pour l'analyse statique et la preuve de code C. Son architecture modulaire permet de réaliser diverses analyses (valeurs possibles d'une variable en un point du programme, slicing, occurrences d'une variable, ...) et preuves (preuve de non débordement des variables entières ou des tableaux, preuve qu'un programme remplit bien une spécification, ...).

Nous ferons une présentation introductive de Frama-C et des outils associés en expliquant la théorie avec les mains et surtout en montrant des exemples.

Plan supposé de l'exposé :

• Motivations
• Préludes : quelques exemples
• Introduction à Frama-C, son architecture
• Analyse statique de code C
• Preuve de code C
• Pour aller plus loin