 |
Cours et Colloques |
Contact:
symposia@inria.fr
JFLA 2012
4 février au 7 février 2012 Carnac
Programme JFLA 2012
Arrivée: 4 février 2012
Premier jour: 4 février 2012
- 14h00 - 15h15 Cocktail de bienvenue
- 15h15 - 15h45 Accueil - Présentation
- 15h45 - 17h15 Cours par Jean-Christophe Filliâtre :
Vérification déductive de programmes avec Why3
La page du cours et des exercices se trouve ici.
- 17h15 - 17h45 Pause-café
- 17h45 - 19h Cours par Matthieu Sozeau :
Classes de types en Coq
- 19h00 Dîner
Deuxième jour: 5 février 2012
- 9h - 10h30 Cours par Jean-Christophe Filliâtre :
Vérification déductive de programmes avec Why3
La page du cours et des exercices se trouve ici.
- 10h30 - 11h Pause-café
- 11h00 - 12h15 Cours par Matthieu Sozeau :
Classes de types en Coq
- 12h30 - 14h Déjeuner
- 14h00 - 18h Excursion: une balade
- 19h00 Dîner
Troisième jour: 6 février 2012
- 9h00 - 10h00 Conférence invitée par Dimitrios Vytiniotis
:
Stop when you are Almost-Full: terminator and size-change
termination in Coq
- 10h - 10h30 Pause-café
- 10h30 - 12h00
- Christophe Deleuze.
Concurrence et continuations en OCaml
- Fabrice Le Fessant et Thomas Gazagnaire.
Gestion de projet avec ocp-build
- Bernard Serpette et Emmanuel Chailloux.
Séparation des couleurs dans un
lambda-calcul bichrome
- 12h00 - 14h Déjeuner
- 14h00 - 15h30
- Simon Boulier et Alan
Schmitt.
Formalisation de
HOCore en Coq
- Daniel De
Rauglaudre.
Vérification
formelle de conditions d'ordonnancabilité de tâches temps réel
périodiques strictes
- Pierre
Boutillier.
Ad hoc reductions
make structural guard condition stricter and smarter
- 15h30 - 16h00 Pause
- 16h00 - 17h00
- Cyril
Cohen.
Construction des nombres
algébriques réels en Coq
- Catherine Lelay et Guillaume Melquiond.
Différentiabilité et
intégrabilité en Coq. Application à la formule de
d'Alembert
- 19h00 Dîner
Quatrième jour: 7 février 2012
- 9h00 - 10h00 Conférence invitée par Benjamin Grégoire :
Easycrypt : un outil pour les preuves de cryptographie exacte
- 10h - 10h30 Pause-café
- 10h30 - 11h30
- Jean-François
Durfourd.
Dérivation de
l'algorithme de Schorr-Waite en Coq par une méthode
algébrique
- Mathieu Jaume et Renaud
Rioboo.
Développement de
systèmes sécurisés avec l'atelier FoCaLiZe
- 11h30 - 12h00 Bilan des journées
- 12h00 - 14h00 Déjeuner
Pour tout renseignement, contacter
Chantal Girodon
INRIA Service IST
Domaine de Voluceau - BP 105
78153 Le Chesnay cedex - France
Tel : +33 (0)1 39 63 50 53 - Fax : +33 (0)1 39 63 56 38
email : symposia@inria.fr
http://jfla.inria.fr/2012/
Pour toutes remarques d'ordre général ou technique concernant
cette page, écrire à Pierre.Weis@inria.fr.
Conception et mise au point: Pierre Weis.
Copyright
© 1996 - 2011 INRIA, tous droits réservés.
Date de dernière modification:
mercredi 1er février 2012
Powered by Caml
