stage_cerpan_automatisation
Sujet de stage
Automatisation de “preuves numériques” en Coq.
Encadrement : Micaela Mayero
Lieu :
| équipe LCR |
| LIPN, CNRS UMR 7030 |
| Université Paris13 |
| 99 avenue Jean-Baptiste Clément |
| 93430 VILLETANEUSE |
Contacts : Micaela.Mayero [@] lipn.univ-paris13.fr
Financement : oui
Ce stage aura lieu dans le cadre de la collaboration avec Sylvie
Boldo (https://www.lri.fr/~sboldo/),
François Clément (https://who.rocq.inria.fr/Francois.Clement/),
Vincent Martin (http://lmac.utc.fr/auteur/vincent-martin) et
Florian Faissole (https://www.lri.fr/~faissole/).
L'objectif est de développer et mettre en application des
méthodes permettant de démontrer formellement la correction de programmes
issus du domaine de l'analyse numérique, en particulier sur les aspets
liés au calcul flottant et aux erreurs de méthode du schéma numérique.
Objectif du stage:
Les preuves de programmes numériques présentent certaines spécificités
récurrentes. Le premier objectif de ce stage sera d'effectuer un tour
d'horizon de ces preuves afin d'identifier les cas les plus
rencontrés, que ce soit dans les preuves utilisant les flottants
(Float) ou celles utlisant les réels (Reals).
Cette étape donnera lieu au second objectif du stage: développer des
tactiques Coq dédiées aux nombres flottants et réels dans le cadre de preuves de
programmes numériques.
Des groupes de travail auront lieu à Orsay et à Paris.
Prérequis: une connaissance de base de Coq sera appréciée.
Sites en rapport avec le projet et le sujet:
http://www-lipn.univ-paris13.fr/LCR/
http://coq.inria.fr/coq-fra.html
http://coquelicot.saclay.inria.fr/
http://labex-digicosme.fr/GT+ELFIC
http://fost.saclay.inria.fr/
http://www-lipn.univ-paris13.fr/CerPAN/
Ce document a été traduit de LATEX par HEVEA
