L'étape d'écriture de la spécification est à la charge de l'utilisateur. Jusqu'à maintenant, la plupart des outils laissaient aussi à la charge de l'utilisateur la tâche de démonter que le programme vérifie bien sa spécification.
Des outils comme Why ou Caduceus permettent, à partir d'un programme et de sa spécification sous forme d'annotations, d'engendrer une série de conjectures qui doivent être vérifiées pour garantir la correction du programme. Ces conjectures permettent de relier les préconditions et post-conditions (au sens de la logique de Hoare) des instructions utilisées dans le programme.
La démonstration de ces conjectures est généralement faite interactivement par l'utilisateur au moyen d'un système d'aide à la preuve. Dans certains cas, il est cependant possible de les démontrer automatiquement en utilisant des procédures de décision comme Simplify ou CVC Lite.
L'objectif de ce travail est d'apprendre à utiliser l'outil Caduceus pour spécifier des programmes écrits en C et d'étudier les possibilités de démontrer automatiquement leur correction au moyen des procédures de décision existantes. On s'intéressera d'abord à des programmes simples comme la recherche d'un élément dans un tableau ou un des programmes classiques de tri d'un tableau. Si le temps le permet, on pourra poursuivre cette étude sur d'autres programmes similaires ou d'un intérêt particulier pour l'étudiant participant à ce travail.