Déduction automatique appliquée à l'analyse et la vérification de systèmes infinis

Laurent Vigneron

Cet exposé présente différents exemples d'applications concrètes de méthodes formelles pour l'analyse et la vérification de systèmes complexes dans des domaines très variés, comme les mathématiques, la normalisation en réécriture et le sécurité des communications.

Laurent Vigneron est Professeur en informatique à l'Université de Lorraine. Après des études en informatique à Nancy et une formation à la recherche fondamentale dans le domaine de l'automatisation du raisonnement en logique du premier ordre, il a travaillé à l'Université de Stony Brook (NY) sur l'analyse automatique d'algèbres approximantes, et la construction de clôture par congruence de systèmes équationnels. De retour à Nancy, il s'est spécialisé dans les applications de la recherche fondamentale, et en particulier l'analyse de protocoles cryptographiques et de compositions de services Web.