Publications : Micaela Mayero
Back| [12] | Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. A Coq formalization of Lebesgue induction principle and Tonelli's theorem. In 25th International Symposium on Formal Methods (FM 2023), volume 14000 of Lecture Notes in Computer Science, pages 39--55, 2023. [ bib | DOI | full text on HAL ] |
| [11] | Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. Lebesgue induction and Tonelli's theorem in Coq. Research Report 9457, Inria, 2023. [ bib | full text on HAL ] |
| [10] | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. Journal of Automated Reasoning, 66:175--213, 2022. [ bib | DOI | full text on HAL ] |
| [9] |
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and
Micaela Mayero.
A Coq formalization of Lebesgue integration of nonnegative
functions.
Research Report RR-9401, Inria, France, 2021.
[ bib |
full text on HAL ]
Keywords: Lebesgue integration ; Measure theory ; Coq ; Formal proof ; Coq ; Preuve formelle ; Théorie de la mesure ; Intégrale de Lebesgue |
| [8] | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. Preuve formelle du théorème de Lax--Milgram. In 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Montpellier, France, June 2017. [ bib | full text on HAL | .pdf ] |
| [7] | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq Formal Proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79--89, New York, NY, USA, January 2017. ACM. [ bib | DOI | full text on HAL | .pdf ] |
| [6] |
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry.
Formally verified certificate checkers for hardest-to-round
computation.
Journal of Automated Reasoning, 54(1):1--29, 2015.
[ bib |
DOI |
full text on HAL ]
Keywords: formal proofs ; certificate checkers ; Hensel's lemma ; modular arithmetic |
| [5] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325--352, 2014. [ bib | DOI | full text on HAL | http ] |
| [4] |
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry.
Formally verified certificate checkers for hardest-to-round
computation.
Journal of Automated Reasoning, pages 1--29, 2014.
[ bib |
DOI |
full text on HAL ]
Keywords: Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic |
| [3] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 50(4):423--456, April 2013. [ bib | DOI | full text on HAL ] |
| [2] |
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela
Mayero, Guillaume Melquiond, and Pierre Weis.
Wave equation numerical resolution: Mathematics and program.
Research Report 7826, INRIA, December 2011.
[ bib |
full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked. Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis |
| [1] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal proof of a wave equation resolution scheme: the method error. In Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 147--162. Springer, 2010. [ bib | DOI | full text on HAL ] |
Back
This page was generated by bibtex2html.