Pierre CASTERAN
Pierre Casteran Maître de Conférences (Université Bordeaux 1)

Équipe LaBRI : Méthodes formelles
Fonction administrative :
Page personnelle : http://www.labri.fr/~casteran
Courrier électronique : pierre.casteranarobaselabri.fr
Bureau : 304
Tél : +33 (0)5 40 00 69 31


Recherche

1) Notations d'Ordinaux et opérateur de description:

En 2005 et 2006, dans le cadre de l'ANR A3PAT ( ANR-05-BLAN-0146), j'ai travaillé
sur les preuves de terminaison à l'aide d'ordinaux. Dans un premier temps,
écriture de modules Coq sur les formes normales de Cantor
(ordinal $\epsilon\sb{0}$) et de Veblen (ordinal $\Gamma\sb{0}$). Ces modules permettent
à la fois le calcul (arithmétique des ordinaux) et la preuve. La preuve
de bonne fondation utilise notamment l'ordre récursif sur les chemins et a été
faite en collaboration avec Evelyne Contéjean (LRI, projet Inria Proval).
A titre de démonstration de cette bibliothèque figure la cersion en Coq des thèorèmes de
terminaion des suites de Goodstein et des bataiiles d'hydres.

La validation des représentations utilisées dans le travail précédent exigeait
la confrontation avec une théorie mathématique bien établie. Pour ce faire,
j'ai implanté en Coq la théorie axiomatique des ordinaux dénombrables de
K. Schütte.

Comme l'ensemble des ordinaux dénombrables ne peut être directement représenté
par un langage de termes finis, ce travail a rendu nécessaire l'écriture
d'outils (lemmes et tactiques) facilitant l'utilisation de l'opérateur de
description d'Hilbert, qui permet l'adjonction de définitions non constructives
dans la logique de Coq.

Ces travaux sont accessibles sous forme de théories Coq (contribution "On ordinal Notations", avec E. Contéjean et par la communication aux JFLA 2007.


2) Preuves formelles de calculs locaux:

A partir de 2007, j'ai rejoint le projet Visidia du LaBRI (M. Mosbah).
Ce projet s'intéresse à un modèle élegant d'algorithmique distribuée,
à l'aide d'une représentation sous forme de systèmes de réétiquetage de graphes
(systèmes de calculs locaux.)

L'idée est de construire un ensemble d'outils facilitant la preuve formelle
en Coq non seulement de systèmes de calcul locaux étudiés dans la littérature,
mais aussi des propriétés génériques de ces systèmes.

Ce travail est au
coeur de la thèse de V. Filou co-dirigée par M. Mosbah et moi-même depuis
Oct. 2008. Il concerne les ANR RIMEL (ANR-06-SETIN-015) (preuves et génération d'algorithmes
par invariants) et A3PAT (techniques de preuves de terminaison).


Cette modélisation nous a déjà permis de prouver entièrement en Coq des
algorithmes distribués de calcul d'arbre recouvrant et d'éléction dans un
arbre. Mais les résultats les plus intéressants consistent la preuve de
propriétés génériques permettant de prouver en Coq l'impossibilité de réaliser
certaines spécifications à l'aide de système de calculs locaux basés sur le
rendez-vous: élection dans un arbre initialement non étiqueté, calcul du dégré
des sommets avec détection locale de la terminaison.

Ce travail est présenté dans la communication au colloque SCCS'09.

Extrait de publications













Page mise à jour le 13/08/2010 à 10:56