Sujet : Vérification de programmes

Responsable : A. Arnold

Téléphone : 05 40 00 60 94

e-mail :mailto:arnold@labri.fr

Équipe : MVTsi

Thème :

 

Présentation du sujet : Il s'agit de faire une étude "bibliographique" sur la vérificationn de programmes.
Il existe des outils permettant de vérifier des programmes écrits en C, en C++ ou en Java. Le travail demandé consistera à recenser le plus grand nombre possible de ces outils, à décrire leur fonctionnalités et, dans la mesure où certains d'entre eux sont librement utilisables, à les installer et à les expérimenter. Un exemple de travail de cette nature est la thèse de Master de Cyrille Artho (voir ci-dessous).
Le but ultime de ce travail est de faire un état de l'art le plus complet possible afin de déterminer les directions de recherches à explorer si on souhaite vérifier non seulement des modèles des fonctionnalités de logiciels à fabriquer, mais les logiciels eux-mêmes.

Mot-clés : Vérification de programmes

Références : Finding faults in multi-threaded programs (Cyrille Artho)

Commentaires éventuels : La thèse de Master de Cyrille Artho (disponible chez A. Arnold) contient la description et l'expérimentation de quelques outils de vérification.