Vérification formelle basée maude du code C

Abstract

Ce travail s'inscrit à l'axe de recherche général de la preuve formelle de la conformité d'un programme impératif écrit en C par rapport à sa spécification en se basant sur les capacités offertes par l'environnement Maude qui est un candidat idéal pour la spécification de système. Notre but est la génération automatique d'une spécification Maude à partir du code C. Cette transformation est faite par l'intermédiaire du graphe de flot de contrôle et de données qui est généré automatiquement à partir du code C. Ce dernier sera utilisé ensuite pour générer automatiquement un module système Maude. Plusieurs propriétés orientées contrôle et données peuvent être vérifiées en utilisant les outils offerts par Maude et en particulier le model checker.