- 9h-9h30 : Accueil des participants
- 9h30 - 10h : Introduction de la journée, présentation rapide du GDR GPL et du groupe LTP, C. Dubois, P. Castéran
- 10h 1ère session :
-
Vérification Interactive de Programmes Fonctionnels
Arthur Chargéraud (Inria Rocquencourt) - Preuve modulaire de programmes impératifs d’ordre supérieur
Johannes Kanig (INRIA Saclay) - Dépasser les limites de la co-récursion gardée par les constructeurs
Yves Bertot (INRIA Sophia Antipolis) - Analyse de flôt d’information pour les systèmes embarqués
Dorina Ghindici (LIFL/Inria Lille - Nord Europe)
-
Vérification Interactive de Programmes Fonctionnels
- 12 h : déjeuner à l’ENSIIE
- 13h30 : 2ème session
- Conception, spécification et preuve formelle d’un algorithme de calcul d’enveloppe convexe avec des hypercartes en Coq
Christophe Brun (LSIIT Strasbourg) - Réécriture topologique, vers une géométrisation de la
programmation
Antoine Spicher (Créteil, LACL) - Vérification de la redécoration pour des matrices triangulaires infinies
en Coq
Ralph Matthes (IRIT, Toulouse)
- Conception, spécification et preuve formelle d’un algorithme de calcul d’enveloppe convexe avec des hypercartes en Coq
- 15h : Pause
- 15h30 : 3ème session
- Un générateur de conditions de vérifications certifié pour un bytecode
Frédéric Besson (IRISA, Rennes) - Interaction avec un gestionnaire de mémoire automatique
Zaynah Dargaye (CEDRIC et INRIA Rocquencourt) - Scalable BIBOP garbage collection for parallel functional programs on multi-core machines
Luca Saiu (LIPN, Paris)
- Un générateur de conditions de vérifications certifié pour un bytecode
- 17h : Discussion, suggestions
- 17h30 : Fin de la journée
ENSIIE, 1 square de la résistance,
91 025 Évry cedex, France.
01 69 36 73 47.