Retour à l'index du GREYC

Séminaire Algorithmique

Site du CNRS

Séminaire Algorithmique

Le séminaire a lieu le mardi à 11 h 45 (sauf modification exceptionnelle), au campus Côte de Nacre, bâtiment Sciences 3, salle S3 351, 3ème étage.

Résumé du séminaire du Mardi 14 Février 2006

Techniques algorithmiques SAT pour la Vérification Formelle

par Samuel Dellacherie (AerieLogic), Bernard Jurkowiak (AerieLogic)

La vérification formelle (encore appelée "model-checking" ou "property checking") regroupe les techniques algorithmiques permettant de vérifier de manière exhaustive les fonctionnalités d'un logiciel ou d'un circuit électronique. Parmis les nombreux algorithmes développés ces 20 dernières années, les techniques SAT ont acquis une place de choix de par leur capacité à résoudre des problèmes de grande taille tout en ayant un niveau d'automatisation élevé.

Nous commencerons notre présentation par une introduction à la vérification formelle en milieu industriel. Ensuite, après un bref tour d'horizon des techniques algorithmiques existantes, nous développerons plus en détails les techniques SAT: ses principes de base ainsi que son utilisation en preuve bornée et en preuve non bornée.

GREYC
Campus Côte de Nacre, boulevard du Maréchal Juin
BP 5186
14032 Caen Cedex
FAX : +33 (0)2 31 56 73 30
http://www.greyc.fr