Séminaires
Séminaire du 14 Novembre 2008
Lieu
ENS de Cachan: comment y aller
La salle se trouve au Pavillon des Jardins.
Programme
14h00-15h00: Stéphane Demri (LSV, ENS de Cachan)
"Logiques temporelles pour les séquences d'états mémoire"
Abstract: Dans le but de vérifier des programmes avec pointeurs, nous introduisons une logique temporelle à la LTL dont les formules atomiques sont issues de de la logique de séparation propositionnelle. Dans cet exposé, nous rappellerons quelques faits marquants sur la logique de séparation ainsi que sur l'approche par automates des logiques temporelles.
Ensuite, notre analyse porte sur la décidabilité et complexité de divers problèmes de model-checking et de satisfaisabilité en considérant par exemple plusieurs fragments de la logique de séparation (incluant par exemple l'arithmétique sur les pointeurs) et plusieurs classes de modèles (avec ou sans tas mémoire constant). Certains problèmes résolubles en espace polynomial sont traités par une approche par automates en utilisant une abstraction idoine des états mémoire dépendant du fragment de la logique de séparation considéré au niveau atomique.
Il s'agit d'un travail commun avec Rémi Brochenin (LSV) et Etienne Lozes (LSV)..
15h00-15h30 : Alban Linard (LIP6/UPMC)
"Un framework pour les diagrammes de décision : application à la génération d'espaces d'état pour les réseaux de Petri symétriques"
Abstract: Les Diagrammes de Décision (DDs) sont des structures de données compactes permettant de manipuler de grands ensembles de données tout en étant efficace en temps. Les DDs sont utilisés avec succès depuis plus de deux décennies, en particulier dans le domaine du model-checking pour représenter des ensembles d'états.
Bien que partageant des principes similaires, différents types de DDs ont vu le jour, correspondant à des types de données et d'analyses différents. Des résultats théoriques et pratiques ont été obtenus indépendamment pour chacun d'eux. Nous proposons une définition de DDs assez générale pour englober un grand nombre de variantes tout en permettant d'exprimer les spécificités propres à chacun.