Evènement pour le groupe Algorithmique Distribuée


Date 2007-05-02  11:00-12:00
TitrePreuve automatique par récurrence sur des structures de données complexes 
RésuméNous proposons avec Adel Bouhoula une nouvelle approche pour l'automatisation de la récurrence sur des structures de données complexes (telles que listes ordonnées, arbres, powerlists...) spécifiées é l'aide d'équations avec conditions et contraintes. Notre procédure est basée sur l'utilisation d'une grammaires d'arbres à contraintes qui décrit exactement le modèle initial de la spécification donnée. Cette grammaire sert à la fois de schéma de récurrence, pour la génération de sous-buts, et pour des vérifications de cohérence durant les étapes de récurrence. La procédure proposée est montrée correcte et réfutationellement complète même en présence d'axiomes contraints entre termes constructeurs, et fournit des preuves très naturelles sur un certains nombre d'exemples.  
LieuSalle 075 
Orateur Florent Jacquemard 
Url LSV - Cachan 



Aucun document lié à cet événement.

Retour
Retour à l'index