Frama-C est un ensemble d’outils pour l’analyse de logiciels C. Dans Frama-C, différentes techniques d’analyse peuvent être implémentées comme plug-ins (greffons) dans un même cadre. La collaboration entre plug-ins repose en partie sur le langage commun de spécification ACSL. Chaque plug-in est supposé interpréter ACSL au mieux de ses possibilités.

Ce post-doctorat consiste à améliorer la précision de l’analyse de valeurs, basée sur la technique d’Interprétation Abstraite, de Frama-C, pour les constructions qui ne sont pas actuellement traitées. Le traitement de certaines constructions nécessitera la conception d’un ou plusieurs domaines abstraits spécifiques.

http://frama-c.com

http://frama-c.com/value.html

http://frama-c.com/acsl.html