Annonce de Seminaire: "Preuve de programmes C par traduction fonctionnelle"

J'ai reçu ça. Ca peut intéresser des parisiens.

Séminaire
Laboratoire Spécification et Vérification
http://www.lsv.ens-cachan.fr/


Mardi 21 mars 2006, à 11 h, Salle de Conférence (Pavillon des Jardins)

Claude Marché (LRI) fera un exposé sur

"Preuve de programmes C par traduction fonctionnelle"

Abstract:

L'approche Why pour la preuve de programmes impératifs consiste à
traduire les programmes (annotés par des spécifications) en des
programmes fonctionnels avec types dépendants. L'outil Why qui
implémente cette approche produit, à partir d'un programme annoté dans
son langage spécifique, un terme Coq équivalent, avec des trous qui sont
les obligations de preuve nécessaires pour établir la correction de ce
programme. Nous expliquons ce mécanisme, puis nous l'appliquons pour des
programmes écrit en langage C. Nous expliquons la modélisation
nécessaire du tas mémoire, pour parvenir à traiter les programmes avec
pointeurs et leur aliasing potentiel.


Marc Boyer
--
Si tu peux supporter d'entendre tes paroles
Travesties par des gueux pour exiter des sots
IF -- Rudyard Kipling (Trad. Paul Éluard)