From LaBRI - Laboratoire Bordelais de Recherche en Informatique

MF: Assistants

Equipe Méthodes Formelles
Logiques, graphes et langages
Assistants de preuves
Responsables : P. Castéran et O. Ly.

Présentation de la direction de recherche

Les assistants de preuve sont particulièrement utiles dans la vérification de composants matériels ou logiciels, et ce pour des propriétés indécidables. Afin de pallier le manque d'automaticité de la vérification, ces outils sont interactifs et accompagnés de langages permettant de programmer des stratégies de démonstration, voire même de disposer de procédures automatiques sur des fragments décidables de la théorie considérée.

L'assistant de preuve Coq est intéressant à plus d'un titre :

Les activités sur cette direction de recherche s'articulent autour des points suivants :

Les activités autour de ce sous-thème comportent donc des aspects pratiques, notamment dans la programmation de méthodes de preuve, et plus fondamentaux, concernant la puissance d'expression de divers formalismes logiques.

Récupéré sur http://www.labri.fr/index.php?n=MF.Assistants
Page mise à jour le 24/10/2009 à 08:18