Applications des assistants de preuve dans la vérification
 
 Les assistants de preuve sont des outils pour faire des 
 preuves semi-automatiques : les étapes de routine sont 
 faites automatiquement, les étapes difficiles sont 
 stipulées par une personne. Un exemple, celui qui est 
 pertinent dans ma recherche, est l'assistant Isabelle.
 Les assistants de preuve sont une grande ligne de recherche
 avec une conférence dédiée : ITP, anciennement TPHOL.
 
 Avant de venir à Toulouse, je me suis occupé de 
 l'utilisation des assistants de preuve pour la vérification 
 des algorithmes du model-checking. En fait, on parle ici 
 des algorithmes classiques sur les automates. Je vais 
 rapporter quelques détails sur un travail que j'ai fait 
 dans ce domaine et sur un projet en Allemagne auquel je
 participe.
 
 Je voudrais continuer cette ligne de recherche et au même 
 temps rajouter des aspects dans lesquels des collègues de 
 l'IRIT sont spécialistes. Pour cela, je voudrais appliquer 
 les assistants de preuve aussi à la vérification des 
 programmes répartis, une vérification qui elle aussi reste 
 sur des automates, dans ce cas là des automates temporisés.