Verification de proprietes sur un programme en utilisant de l'analyse statique et de la verification de modele

Auteurs

Aymeric Fages

Type

techreport

Année

2020

Numéro

2020

Résumé

Dans ce papier, nous presentons les differentes solutions pour transformer un programme en un systeme d'etats finis. Puis nous presentons notre programme fonctionnel qui nous permet de dire si un programme en C verifie ou non une formule LTL. Nous decrivons tous les aspect de ce programme, que ce soit de l'utilisation de LLVM, d'un algorithme C++ d'abstraction de modeles ou encore de la bibliotheque Spot. Dans une premiere partie, nous expliquons quel type de graphe fini nous voulons obtenir comme modele du programme. Dans une deuxieme partie, nous definissons des notions importantes de la verification de modeles, tels que les systemes de poussee ou les automates de Buchi. Dans une troisieme partie, nous expliquons comment trouver une sous-approximation et sur-approximation d'un systeme de poussee vers un systeme d'etats finis. Pour finir, nous montrons comment ces solutions theoriques sont implementees en un vrai programme fonctionnel