(programme et emploi du temps ici)
En plus des cours, il y a aura deux exposés sur des thématiques connexes aux cours.
L’Assistant Coq : une boite à outils pour l’ingénierie des preuves
- Christine PAULIN-MOHRING (LRI, Université Paris-Sud)
Nous présenterons les principaux éléments qui constituent l’assistant de preuve Coq : les constructions de base du langage et l’environnement de preuve. Nous illustrerons les relations possibles entre preuve interactive et automatique à travers la technique de preuve réflexive. Nous montrerons également les possibilités de modélisation avancée à travers l’exemple de la représentation de programmes aléatoires.
Questions de décidabilité sur les modèles temporisés, une application des techniques de calcul formel
- Béatrice BÉRARD (LIP6)
Cet exposé sera centré sur la notion de quotient. Il partira de l’exemple des automates finis, et de la méthode générale de construction d’un quotient, qui permet de réduire un système infini à des fins de vérification. Après une présentation des systèmes hybrides, qui manipulent des variables évoluant continument en fonction du temps, et susceptibles également de changements discrets, nous montrerons la construction maintenant classique du graphe des régions d’Aur et Dill, qui produit un quotient pour les automates temporisés. Puis, sur une classe de modèles introduite plus récemment, celle des automates temporisés à interruption, nous verrons une construction de quotient reposant sur un principe un peu différent. En montrant le lien avec la décomposition cylindrique, nous présenterons finalement une classe qui généralise les automates à interruptions en utilisant des polynomes d’horloges, et pour laquelle l’accessibilité reste décidable.
