mayero.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc mayero.cite -ob mayero.bib -c 'author : "mayero"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@article{boldo14camwa,
title = {{Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Filli{\^a}tre, Jean-Christophe and Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
year = {2014},
volume = {68},
number = {3},
pages = {325--352},
journal = {Computers and Mathematics with Applications},
hal = {http://hal.inria.fr/hal-00769201},
url = {http://www.sciencedirect.com/science/article/pii/S0898122114002636},
doi = {10.1016/j.camwa.2014.06.004},
topics = {team,lri},
type_publi = {irevcomlec}
}
@inproceedings{boldo10-itp,
author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
title = {Formal Proof of a Wave Equation Resolution Scheme: the Method Error},
booktitle = {Interactive Theorem Proving},
year = 2010,
series = {Lecture Notes in Computer Science},
x-address = {Edinburgh, Scotland},
x-month = jul,
publisher = {Springer},
x-editor = {Matt Kaufmann and Lawrence C. Paulson},
volume = 6172,
pages = {147--162},
hal = {http://hal.inria.fr/inria-00450789/en},
doi = {10.1007/978-3-642-14052-5_12/},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-cle-support = {ITProving},
x-type = {article},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@techreport{BCFMMW11rr,
hal_id = {hal-00649240},
hal = {http://hal.inria.fr/hal-00649240/en/},
title = {Wave Equation Numerical Resolution: Mathematics and Program},
author = {Boldo, Sylvie and Cl\'ement, Fran\c{c}ois and Filli{\^a}tre, Jean-Christophe and Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
abstract = {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},
language = {Anglais},
affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI , ESTIME - INRIA Rocquencourt , Laboratoire d'informatique de Paris-nord - LIPN , ARENAIRE - Inria Grenoble Rh{\^o}ne-Alpes / LIP Laboratoire de l'Informatique du Parall{\'e}lisme},
pages = {30},
type = {Research Report},
institution = {INRIA},
number = 7826,
year = 2011,
month = dec,
topics = {team},
x-equipes = {demons PROVAL ext},
x-support = {rapport}
}
@article{boldo13jar,
author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
title = {Wave Equation Numerical Resolution:
a Comprehensive Mechanized Proof of a {C} Program},
journal = {Journal of Automated Reasoning},
year = {2013},
volume = {50},
number = {4},
pages = {423--456},
month = apr,
x-international-audience = {yes},
x-editorial-board = {yes},
x-equipes = {demons PROVAL ext},
x-support = {revue},
x-type = {article},
x-cle-support = {JAR},
hal = {http://hal.inria.fr/hal-00649240/en/},
doi = {10.1007/s10817-012-9255-4},
topics = {team}
}
@article{martindorel14jar,
topics = {team},
hal = {http://hal.inria.fr/hal-00919498},
year = 2014,
journal = {Journal of Automated Reasoning},
doi = {10.1007/s10817-014-9312-2},
title = {Formally Verified Certificate Checkers for Hardest-to-Round Computation},
publisher = {Springer Netherlands},
keywords = {Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic},
author = {Martin-Dorel, {\'E}rik and Hanrot, Guillaume and Mayero, Micaela and Th{\'e}ry, Laurent},
pages = {1--29},
language = {English}
}
@article{martindorel15jarb,
topics = {team},
title = {Formally verified certificate checkers for hardest-to-round computation},
author = {Martin-Dorel, {\'E}rik and Hanrot, Guillaume and Mayero, Micaela and Th{\'e}ry, Laurent},
hal = {https://hal.inria.fr/hal-00919498},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 54,
number = 1,
pages = {1-29},
year = 2015,
doi = {10.1007/s10817-014-9312-2},
keywords = {formal proofs ; certificate checkers ; Hensel's lemma ; modular arithmetic}
}
@inproceedings{boldo:hal-01391578,
topics = {team},
title = {{A Coq Formal Proof of the Lax-Milgram theorem}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian
and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.inria.fr/hal-01391578},
booktitle = {{Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
series = {CPP 2017},
location = {Paris, France},
year = {2017},
month = jan,
pages = {79--89},
pdf = {https://hal.inria.fr/hal-01391578/file/article.pdf},
doi = {10.1145/3018610.3018625},
publisher = {ACM},
address = {New York, NY, USA}
}
@inproceedings{BCF17b,
topics = {team},
title = {Preuve formelle du th{\'e}or{\`e}me de {Lax--Milgram}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.archives-ouvertes.fr/hal-01581807},
booktitle = {{16{\`e}mes journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels}},
address = {Montpellier, France},
year = {2017},
month = jun,
pdf = {https://hal.archives-ouvertes.fr/hal-01581807/file/article_afadl.pdf}
}
@techreport{boldo21rr,
topics = {team},
title = {A {Coq} Formalization of {Lebesgue} Integration of Nonnegative Functions},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.inria.fr/hal-03194113},
type = {Research Report},
number = {RR-9401},
institution = {Inria, France},
year = 2021,
keywords = {Lebesgue integration ; Measure theory ; Coq ; Formal proof ; Coq ; Preuve formelle ; Th{\'e}orie de la mesure ; Int{\'e}grale de Lebesgue}
}
@article{boldo22jar,
topics = {team},
title = {A {Coq} Formalization of {Lebesgue} Integration of Nonnegative Functions},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.inria.fr/hal-03471095},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 66,
pages = {175--213},
year = 2022,
doi = {10.1007/s10817-021-09612-0}
}
@inproceedings{boldo23fm,
topics = {team},
title = {A {Coq} Formalization of {Lebesgue} Induction Principle and {Tonelli's} Theorem},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Martin, Vincent and Mayero, Micaela and Mouhcine, Houda},
hal = {https://hal.inria.fr/hal-03889276},
booktitle = {25th International Symposium on Formal Methods (FM 2023)},
series = {Lecture Notes in Computer Science},
volume = 14000,
pages = {39--55},
year = 2023,
doi = {10.1007/978-3-031-27481-7\_4}
}
@techreport{boldo23rr,
topics = {team},
title = {{Lebesgue} Induction and {Tonelli}'s Theorem in {Coq}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Martin, Vincent and Mayero, Micaela and Mouhcine, Houda},
hal = {https://inria.hal.science/hal-03564379},
type = {Research Report},
number = 9457,
institution = {Inria},
year = 2023
}