Micaela Mayero

      

Contacts:

LIPN - UMR CNRS 7030
Institut Galilée - Université Paris Nord
99 avenue Jean-Baptiste Clément
93430 Villetaneuse
FRANCE

Tél.
Fax
: +33 (0) 1 49 40 36 91
: +33 (0) 1 48 26 07 12
Micaela.Mayero [at] lipn.univ-paris13.fr
Bureau
: A209


English version

Last modified: Fri Oct 4 17:15:49 CEST 2013
Je m'intéresse aux preuves formelles et en particulier à l'utilisation des systèmes d'aide à la preuve dans divers domaines, avec lesquels il se développe des interactions, tels que le calcul formel, les mathématiques, la vérification, le hardware, les nombres réels et flottants, ...

Mon outil d'aide à la preuve favori est Coq. J'ai effectué ma thèse dans l'équipe qui développe cet outil. Je l'utilise ou l'ai utilisé dans les travaux suivants (voir les publications pour plus de détails):
  • Participation au projet Coquelicot (nouvelle bibliothèque de nombres réels en Coq)
  • Développement de la bibliothèque CoqApprox dans le cadre du projet TaMaDi
  • Preuve formelle de programme de combinatoire algébrique (logiciel SCHUR)
  • Certification de programmes d'analyse numérique dans le cadre du projet CerPAN que j'ai coordonné et du projet FOST
  • Preuve formelle de raffinement de réseaux de Petri
  • Preuve formelle du théorème des trois intervalles
  • Utilisation dans le cadre de la différentiation automatique
  • Développement de la bibliothèque des nombres réels de Coq
  • Développement de tactiques (automatisation de Coq et de PVS)
  • Interaction entre Coq et Maple
  • Preuve formelle du 20ème problème de Diophante et
    du théorème de Fermat pour n=4 [draft]
  • ...