Menu
Support
Objectif
L’automatisation des preuves par récurrence est un sujet important en informatique et plus particulièrement dans le domaine de la vérification de logiciels et de systèmes. En effet, la plupart des programmes qui ne peuvent être modélisés par des systèmes finis ne peuvent être vérifiés qu’à l’aide d’une récurrence sur les structures de données. Les objectifs du projet sont :- la conception et la réalisation d’un système de démonstration automatique basée sur les techniques de preuves par récurrence et les automates d’arbres à contraintes.
- l’application de ce système à la validation des protocoles et des systèmes distribués.
25.09.2006. 14:31
Participants
Le projet implique des partenaires de trois sites:
- l'École Supérieure des Communications de Tunis. Responsable: Adel Bouhoula
- l'INRIA Futurs, projet SECSI localisé au Laboratoire Spécification et Vérification (LSV), UMR 8643 CNRS ENS de Cachan. Responsable: Florent Jacquemard
- le Laboratoire Bordelais de Recherche en Informatique (LaBRI), UMR 5800 CNRS, Bordeaux I, ENSEIRB. Responsable: Mohamed Mosbah
22.09.2006. 11:25