Séminaire du LIF
Jeudi 6 février à 14h - CMI, Amphi C101
Solange Coupet-Grimal
LIF, équipe MoVe
Preuve formelle d'un récupérateur de mémoire pour cartes à puces
Nous vérifions formellement un récupérateur de mémoire incrémental, variante du célèbre algorithme à 3 couleurs de Dijkstra, avec l'assistant de preuve Coq.
L'exposé illustrera une démarche générale de spécification de systèmes concurrents critiques, de preuve de correction en logique temporelle, et de vérification de la preuve en théorie des types. Nous présenterons à cette occasion une axiomatisation de la logique temporelle linéaire et des ensembles finis dans le calcul des constructions, sous-jacent à Coq.
Ce travail à l'origine motivé par l'extension de la plateforme Java Card à la gestion dynamique de mémoire, s'applique plus généralement à des systèmes temps réel et/ou avec une mémoire virtuellement infinie comme Internet.
Aucun pré-requis n'est nécessaire à la compréhension de l'exposé.
Home page : http://www.cmi.univ-mrs.fr/~solange/
An Axiomatization of Linear Temporal Logic in The Calculus of Inductive Constructions, to appear in The Journal of Logic and Computation.
Formal Verification of an Incremental Garbage Collector, with Catherine Nouvet, to appear in The Journal of Logic and Computation.