Micaela Mayero Homepage

Je m'intéresse aux preuves formelles et en particulier à l'utilisation des systèmes d'aide à la preuve dans divers domaines tels que le calcul formel, les mathématiques, la vérification, le hardware, ...

Mon outil d'aide à la preuve favori est Coq. J'ai effectué ma thèse au sein de l'équipe LogiCal, qui développe cet outil. Je l'utilise ou l'ai utilisé dans les travaux suivants (voir les publications pour plus de détails):

Certification de programmes d'analyse numérique dans le cadre du projet CerPAN que je coordonne et du projet FOST.
Preuve formelle de raffinement de réseaux de Petri [1]
Preuve formelle du théorème des trois intervalles [5, 6, 8, 10]
Utilisation dans le cadre de la différentiation automatique [3, 8]
Développement de la bibliothèque des nombres réels de Coq [8, 9]
Développement de tactiques (automatisation de Coq et de PVS) [1, 4, 8, 7, 9]
Interaction entre Coq et Maple [1, 2]
Preuve formelle du 20ème problème de Diophante et
du théorème de Fermat pour n=4 [draft]
...