Sujet : Conception Formelle en PVS



Responsable : Pierre Castéran
Téléphone : 05 40 00 69 31

e-mail : pierre.casteran@labri.fr

Présentation du sujet : Il s'agit d'étudier l'adéquation du système PVS (Prototype Verification System) à la présentation des notions de développement de programmes prouvés et de raffinement.

PVS est un système pour la vérification de logiciel en open-source, comportant un prouveur semi-automatique. Ses applications principales sont la vérification de matériel, de protocoles, et de systèmes critiques.
Par ailleurs, il a été développé un outil appelé PBS, écrit en Ocaml, permettant de traduire les machines abstraites de B en théorie PVS.

Travail à faire :

Il consistera à :


Mot-clés : Conception formelle, Preuves, Logiciel libre.