Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Sylvie Boldo
@article{DBLP:journals/actanum/BoldoJMM23,
author = {Sylvie Boldo and
Claude{-}Pierre Jeannerod and
Guillaume Melquiond and
Jean{-}Michel Muller},
title = {Floating-point arithmetic},
journal = {Acta Numer.},
volume = {32},
pages = {203--290},
year = {2023},
url = {https://doi.org/10.1017/S0962492922000101},
doi = {10.1017/S0962492922000101},
timestamp = {Fri, 02 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/actanum/BoldoJMM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/BoldoCMMM23,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Vincent Martin and
Micaela Mayero and
Houda Mouhcine},
editor = {Marsha Chechik and
Joost{-}Pieter Katoen and
Martin Leucker},
title = {A Coq Formalization of Lebesgue Induction Principle and Tonelli's
Theorem},
booktitle = {Formal Methods - 25th International Symposium, {FM} 2023, L{\"{u}}beck,
Germany, March 6-10, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14000},
pages = {39--55},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-27481-7\_4},
doi = {10.1007/978-3-031-27481-7\_4},
timestamp = {Sat, 11 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/fm/BoldoCMMM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BoldoCFMM22,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Florian Faissole and
Vincent Martin and
Micaela Mayero},
title = {A Coq Formalization of Lebesgue Integration of Nonnegative Functions},
journal = {J. Autom. Reason.},
volume = {66},
number = {2},
pages = {175--213},
year = {2022},
url = {https://doi.org/10.1007/s10817-021-09612-0},
doi = {10.1007/S10817-021-09612-0},
timestamp = {Wed, 27 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BoldoCFMM22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tetc/Salem-KnappBW22,
author = {Louise Ben Salem{-}Knapp and
Sylvie Boldo and
William Weens},
title = {Bounding the Round-Off Error of the Upwind Scheme for Advection},
journal = {{IEEE} Trans. Emerg. Top. Comput.},
volume = {10},
number = {3},
pages = {1253--1262},
year = {2022},
url = {https://doi.org/10.1109/TETC.2022.3191472},
doi = {10.1109/TETC.2022.3191472},
timestamp = {Thu, 22 Sep 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tetc/Salem-KnappBW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/Salem-KnappBW22,
author = {Louise Ben Salem{-}Knapp and
Sylvie Boldo and
William Weens},
title = {Bounding the Round-Off Error of the Upwind Scheme for Advection},
booktitle = {29th {IEEE} Symposium on Computer Arithmetic, {ARITH} 2022, Lyon,
France, September 12-14, 2022},
pages = {127},
publisher = {{IEEE}},
year = {2022},
url = {https://doi.org/10.1109/ARITH54963.2022.00031},
doi = {10.1109/ARITH54963.2022.00031},
timestamp = {Thu, 29 Dec 2022 15:06:50 +0100},
biburl = {https://dblp.org/rec/conf/arith/Salem-KnappBW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2201-03242,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Louise Leclerc},
title = {A Coq Formalization of the Bochner integral},
journal = {CoRR},
volume = {abs/2201.03242},
year = {2022},
url = {https://arxiv.org/abs/2201.03242},
eprinttype = {arXiv},
eprint = {2201.03242},
timestamp = {Thu, 20 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2201-03242.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2202-05040,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Vincent Martin and
Micaela Mayero and
Houda Mouhcine},
title = {Lebesgue Induction and Tonelli's Theorem in Coq},
journal = {CoRR},
volume = {abs/2202.05040},
year = {2022},
url = {https://arxiv.org/abs/2202.05040},
eprinttype = {arXiv},
eprint = {2202.05040},
timestamp = {Fri, 18 Feb 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2202-05040.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tc/BoldoLM21,
author = {Sylvie Boldo and
Christoph Quirin Lauter and
Jean{-}Michel Muller},
title = {Emulating Round-to-Nearest Ties-to-Zero "Augmented" Floating-Point
Operations Using Round-to-Nearest Ties-to-Even Arithmetic},
journal = {{IEEE} Trans. Computers},
volume = {70},
number = {7},
pages = {1046--1058},
year = {2021},
url = {https://doi.org/10.1109/TC.2020.3002702},
doi = {10.1109/TC.2020.3002702},
timestamp = {Tue, 15 Jun 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tc/BoldoLM21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoM21,
author = {Sylvie Boldo and
Guillaume Melquiond},
title = {Some Formal Tools for Computer Arithmetic: Flocq and Gappa},
booktitle = {28th {IEEE} Symposium on Computer Arithmetic, {ARITH} 2021, Lyngby,
Denmark, June 14-16, 2021},
pages = {111--114},
publisher = {{IEEE}},
year = {2021},
url = {https://doi.org/10.1109/ARITH51176.2021.00031},
doi = {10.1109/ARITH51176.2021.00031},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/BoldoM21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2104-05256,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Florian Faissole and
Vincent Martin and
Micaela Mayero},
title = {A Coq Formalization of Lebesgue Integration of Nonnegative Functions},
journal = {CoRR},
volume = {abs/2104.05256},
year = {2021},
url = {https://arxiv.org/abs/2104.05256},
eprinttype = {arXiv},
eprint = {2104.05256},
timestamp = {Mon, 19 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2104-05256.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/na/Gallois-WongBC20,
author = {Diane Gallois{-}Wong and
Sylvie Boldo and
Pascal Cuoq},
title = {Optimal inverse projection of floating-point addition},
journal = {Numer. Algorithms},
volume = {83},
number = {3},
pages = {957--986},
year = {2020},
url = {https://doi.org/10.1007/s11075-019-00711-z},
doi = {10.1007/S11075-019-00711-Z},
timestamp = {Sat, 25 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/na/Gallois-WongBC20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tc/BoldoFC20,
author = {Sylvie Boldo and
Florian Faissole and
Alexandre Chapoutot},
title = {Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta
Methods},
journal = {{IEEE} Trans. Computers},
volume = {69},
number = {12},
pages = {1745--1756},
year = {2020},
url = {https://doi.org/10.1109/TC.2019.2917902},
doi = {10.1109/TC.2019.2917902},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tc/BoldoFC20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoGH20,
author = {Sylvie Boldo and
Diane Gallois{-}Wong and
Thibault Hilaire},
title = {A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm},
booktitle = {27th {IEEE} Symposium on Computer Arithmetic, {ARITH} 2020, Portland,
OR, USA, June 7-10, 2020},
pages = {9--16},
publisher = {{IEEE}},
year = {2020},
url = {https://doi.org/10.1109/ARITH48897.2020.00011},
doi = {10.1109/ARITH48897.2020.00011},
timestamp = {Thu, 03 Sep 2020 10:17:40 +0200},
biburl = {https://dblp.org/rec/conf/arith/BoldoGH20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/arith/2019,
editor = {Naofumi Takagi and
Sylvie Boldo and
Martin Langhammer},
title = {26th {IEEE} Symposium on Computer Arithmetic, {ARITH} 2019, Kyoto,
Japan, June 10-12, 2019},
publisher = {{IEEE}},
year = {2019},
url = {https://ieeexplore.ieee.org/xpl/conhome/8864032/proceeding},
isbn = {978-1-7281-3366-9},
timestamp = {Tue, 22 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/arith/2019.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoFT18,
author = {Sylvie Boldo and
Florian Faissole and
Vincent Tourneur},
title = {A Formally-Proved Algorithm to Compute the Correct Average of Decimal
Floating-Point Numbers},
booktitle = {25th {IEEE} Symposium on Computer Arithmetic, {ARITH} 2018, Amherst,
MA, USA, June 25-27, 2018},
pages = {69--75},
publisher = {{IEEE}},
year = {2018},
url = {https://doi.org/10.1109/ARITH.2018.8464761},
doi = {10.1109/ARITH.2018.8464761},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/BoldoFT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/Gallois-WongBH18,
author = {Diane Gallois{-}Wong and
Sylvie Boldo and
Thibault Hilaire},
editor = {Florian Rabe and
William M. Farmer and
Grant O. Passmore and
Abdou Youssef},
title = {A Coq Formalization of Digital Filters},
booktitle = {Intelligent Computer Mathematics - 11th International Conference,
{CICM} 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11006},
pages = {87--103},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-96812-4\_8},
doi = {10.1007/978-3-319-96812-4\_8},
timestamp = {Fri, 20 Nov 2020 16:08:55 +0100},
biburl = {https://dblp.org/rec/conf/mkm/Gallois-WongBH18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/daglib/0041425,
author = {Sylvie Boldo and
Guillaume Melquiond},
title = {Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms
with the Coq System},
publisher = {{ISTE} Press},
year = {2017},
url = {https://www.elsevier.com/books/computer-arithmetic-and-formal-proofs/boldo/978-1-78548-112-3},
isbn = {978-1-7854-8112-3},
timestamp = {Fri, 28 Jun 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/daglib/0041425.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/toms/BoldoGM17,
author = {Sylvie Boldo and
Stef Graillat and
Jean{-}Michel Muller},
title = {On the Robustness of the 2Sum and Fast2Sum Algorithms},
journal = {{ACM} Trans. Math. Softw.},
volume = {44},
number = {1},
pages = {4:1--4:14},
year = {2017},
url = {https://doi.org/10.1145/3054947},
doi = {10.1145/3054947},
timestamp = {Tue, 16 Aug 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/toms/BoldoGM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoFC17,
author = {Sylvie Boldo and
Florian Faissole and
Alexandre Chapoutot},
editor = {Neil Burgess and
Javier D. Bruguera and
Florent de Dinechin},
title = {Round-off Error Analysis of Explicit One-Step Numerical Integration
Methods},
booktitle = {24th {IEEE} Symposium on Computer Arithmetic, {ARITH} 2017, London,
United Kingdom, July 24-26, 2017},
pages = {82--89},
publisher = {{IEEE} Computer Society},
year = {2017},
url = {https://doi.org/10.1109/ARITH.2017.22},
doi = {10.1109/ARITH.2017.22},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/BoldoFC17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BoldoCFMM17,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Florian Faissole and
Vincent Martin and
Micaela Mayero},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {A Coq formal proof of the LaxMilgram theorem},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {79--89},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018625},
doi = {10.1145/3018610.3018625},
timestamp = {Tue, 06 Nov 2018 16:59:23 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BoldoCFMM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BoldoJMP17,
author = {Sylvie Boldo and
Mioara Joldes and
Jean{-}Michel Muller and
Valentina Popescu},
editor = {Mauricio Ayala{-}Rinc{\'{o}}n and
C{\'{e}}sar A. Mu{\~{n}}oz},
title = {Formal Verification of a Floating-Point Expansion Renormalization
Algorithm},
booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}
2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10499},
pages = {98--113},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-66107-0\_7},
doi = {10.1007/978-3-319-66107-0\_7},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/BoldoJMP17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2017nsv,
editor = {Alessandro Abate and
Sylvie Boldo},
title = {Numerical Software Verification - 10th International Workshop, {NSV}
2017, Heidelberg, Germany, July 22-23, 2017, Proceedings [collocated
with {CAV} 2017]},
series = {Lecture Notes in Computer Science},
volume = {10381},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-63501-9},
doi = {10.1007/978-3-319-63501-9},
isbn = {978-3-319-63500-2},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/2017nsv.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mscs/BoldoLM16,
author = {Sylvie Boldo and
Catherine Lelay and
Guillaume Melquiond},
title = {Formalization of real analysis: a survey of proof assistants and libraries},
journal = {Math. Struct. Comput. Sci.},
volume = {26},
number = {7},
pages = {1196--1233},
year = {2016},
url = {https://doi.org/10.1017/S0960129514000437},
doi = {10.1017/S0960129514000437},
timestamp = {Wed, 01 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mscs/BoldoLM16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/Boldo16,
author = {Sylvie Boldo},
editor = {Sergiy Bogomolov and
Matthieu Martel and
Pavithra Prabhakar},
title = {Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest},
booktitle = {Numerical Software Verification - 9th International Workshop, {NSV}
2016, Toronto, ON, Canada, July 17-18, 2016, [collocated with {CAV}
2016], Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {10152},
pages = {47--51},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-54292-8\_4},
doi = {10.1007/978-3-319-54292-8\_4},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/Boldo16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BoldoJLM15,
author = {Sylvie Boldo and
Jacques{-}Henri Jourdan and
Xavier Leroy and
Guillaume Melquiond},
title = {Verified Compilation of Floating-Point Computations},
journal = {J. Autom. Reason.},
volume = {54},
number = {2},
pages = {135--163},
year = {2015},
url = {https://doi.org/10.1007/s10817-014-9317-x},
doi = {10.1007/S10817-014-9317-X},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BoldoJLM15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mics/BoldoLM15,
author = {Sylvie Boldo and
Catherine Lelay and
Guillaume Melquiond},
title = {Coquelicot: {A} User-Friendly Library of Real Analysis for Coq},
journal = {Math. Comput. Sci.},
volume = {9},
number = {1},
pages = {41--62},
year = {2015},
url = {https://doi.org/10.1007/s11786-014-0181-1},
doi = {10.1007/S11786-014-0181-1},
timestamp = {Wed, 12 Aug 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mics/BoldoLM15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfem/Boldo15,
author = {Sylvie Boldo},
editor = {Michael J. Butler and
Sylvain Conchon and
Fatiha Za{\"{\i}}di},
title = {Formal Verification of Programs Computing the Floating-Point Average},
booktitle = {Formal Methods and Software Engineering - 17th International Conference
on Formal Engineering Methods, {ICFEM} 2015, Paris, France, November
3-5, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9407},
pages = {17--32},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-25423-4\_2},
doi = {10.1007/978-3-319-25423-4\_2},
timestamp = {Sun, 02 Jun 2019 21:19:43 +0200},
biburl = {https://dblp.org/rec/conf/icfem/Boldo15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/hal/Boldo14,
author = {Sylvie Boldo},
title = {Deductive Formal Verification: How To Make Your Floating-Point Programs
Behave},
year = {2014},
url = {https://tel.archives-ouvertes.fr/tel-01089643},
timestamp = {Sat, 30 Sep 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/hal/Boldo14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cma/BoldoCFMMW14,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Jean{-}Christophe Filli{\^{a}}tre and
Micaela Mayero and
Guillaume Melquiond and
Pierre Weis},
title = {Trusting computations: {A} mechanized proof from partial differential
equations to actual program},
journal = {Comput. Math. Appl.},
volume = {68},
number = {3},
pages = {325--352},
year = {2014},
url = {https://doi.org/10.1016/j.camwa.2014.06.004},
doi = {10.1016/J.CAMWA.2014.06.004},
timestamp = {Thu, 11 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/cma/BoldoCFMMW14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/Boldo15,
author = {Sylvie Boldo},
editor = {Sergiy Bogomolov and
Matthieu Martel},
title = {Stupid is as Stupid Does: Taking the Square Root of the Square of
a Floating-Point Number},
booktitle = {Seventh and Eighth International Workshops on Numerical Software Verification,
{NSV} 2014, Vienna, Austria, July 17-18, 2014 {\&} {NSV} 2015,
Seattle, WA, USA, April 13, 2015},
series = {Electronic Notes in Theoretical Computer Science},
volume = {317},
pages = {27--32},
publisher = {Elsevier},
year = {2014},
url = {https://doi.org/10.1016/j.entcs.2015.10.004},
doi = {10.1016/J.ENTCS.2015.10.004},
timestamp = {Thu, 10 Nov 2022 15:22:15 +0100},
biburl = {https://dblp.org/rec/journals/entcs/Boldo15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BoldoCFMMW13,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Jean{-}Christophe Filli{\^{a}}tre and
Micaela Mayero and
Guillaume Melquiond and
Pierre Weis},
title = {Wave Equation Numerical Resolution: {A} Comprehensive Mechanized Proof
of a {C} Program},
journal = {J. Autom. Reason.},
volume = {50},
number = {4},
pages = {423--456},
year = {2013},
url = {https://doi.org/10.1007/s10817-012-9255-4},
doi = {10.1007/S10817-012-9255-4},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BoldoCFMMW13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/Boldo13,
author = {Sylvie Boldo},
editor = {Alberto Nannarelli and
Peter{-}Michael Seidel and
Ping Tak Peter Tang},
title = {How to Compute the Area of a Triangle: {A} Formal Revisit},
booktitle = {21st {IEEE} Symposium on Computer Arithmetic, {ARITH} 2013, Austin,
TX, USA, April 7-10, 2013},
pages = {91--98},
publisher = {{IEEE} Computer Society},
year = {2013},
url = {https://doi.org/10.1109/ARITH.2013.29},
doi = {10.1109/ARITH.2013.29},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/Boldo13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoJLM13,
author = {Sylvie Boldo and
Jacques{-}Henri Jourdan and
Xavier Leroy and
Guillaume Melquiond},
editor = {Alberto Nannarelli and
Peter{-}Michael Seidel and
Ping Tak Peter Tang},
title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
booktitle = {21st {IEEE} Symposium on Computer Arithmetic, {ARITH} 2013, Austin,
TX, USA, April 7-10, 2013},
pages = {107--115},
publisher = {{IEEE} Computer Society},
year = {2013},
url = {https://doi.org/10.1109/ARITH.2013.30},
doi = {10.1109/ARITH.2013.30},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/BoldoJLM13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BoldoLM12,
author = {Sylvie Boldo and
Catherine Lelay and
Guillaume Melquiond},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Improving Real Analysis in Coq: {A} User-Friendly Approach to Integrals
and Derivatives},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {289--304},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_22},
doi = {10.1007/978-3-642-35308-6\_22},
timestamp = {Wed, 07 Dec 2022 23:14:04 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BoldoLM12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BoldoCFMMW12,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Jean{-}Christophe Filli{\^{a}}tre and
Micaela Mayero and
Guillaume Melquiond and
Pierre Weis},
title = {Trusting Computations: a Mechanized Proof from Partial Differential
Equations to Actual Program},
journal = {CoRR},
volume = {abs/1212.6641},
year = {2012},
url = {http://arxiv.org/abs/1212.6641},
eprinttype = {arXiv},
eprint = {1212.6641},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BoldoCFMMW12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/isse/BoldoN11,
author = {Sylvie Boldo and
Thi Minh Tuyen Nguyen},
title = {Proofs of numerical programs when the compiler optimizes},
journal = {Innov. Syst. Softw. Eng.},
volume = {7},
number = {2},
pages = {151--160},
year = {2011},
url = {https://doi.org/10.1007/s11334-011-0151-6},
doi = {10.1007/S11334-011-0151-6},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/isse/BoldoN11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mics/BoldoM11,
author = {Sylvie Boldo and
Claude March{\'{e}}},
title = {Formal Verification of Numerical Programs: From {C} Annotated Programs
to Mechanical Proofs},
journal = {Math. Comput. Sci.},
volume = {5},
number = {4},
pages = {377--393},
year = {2011},
url = {https://doi.org/10.1007/s11786-011-0099-9},
doi = {10.1007/S11786-011-0099-9},
timestamp = {Wed, 12 Aug 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mics/BoldoM11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tc/BoldoM11,
author = {Sylvie Boldo and
Jean{-}Michel Muller},
title = {Exact and Approximated Error of the {FMA}},
journal = {{IEEE} Trans. Computers},
volume = {60},
number = {2},
pages = {157--164},
year = {2011},
url = {https://doi.org/10.1109/TC.2010.139},
doi = {10.1109/TC.2010.139},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tc/BoldoM11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoM10,
author = {Sylvie Boldo and
Guillaume Melquiond},
editor = {Elisardo Antelo and
David Hough and
Paolo Ienne},
title = {Flocq: {A} Unified Library for Proving Floating-Point Algorithms in
Coq},
booktitle = {20th {IEEE} Symposium on Computer Arithmetic, {ARITH} 2011, T{\"{u}}bingen,
Germany, 25-27 July 2011},
pages = {243--252},
publisher = {{IEEE} Computer Society},
year = {2011},
url = {https://doi.org/10.1109/ARITH.2011.40},
doi = {10.1109/ARITH.2011.40},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/BoldoM10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1112-1795,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Jean{-}Christophe Filli{\^{a}}tre and
Micaela Mayero and
Guillaume Melquiond and
Pierre Weis},
title = {Wave Equation Numerical Resolution: Mathematics and Program},
journal = {CoRR},
volume = {abs/1112.1795},
year = {2011},
url = {http://arxiv.org/abs/1112.1795},
eprinttype = {arXiv},
eprint = {1112.1795},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1112-1795.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BoldoCFMMW10,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Jean{-}Christophe Filli{\^{a}}tre and
Micaela Mayero and
Guillaume Melquiond and
Pierre Weis},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {Formal Proof of a Wave Equation Resolution Scheme: The Method Error},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {147--162},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_12},
doi = {10.1007/978-3-642-14052-5\_12},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/BoldoCFMMW10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/nfm/BoldoN10,
author = {Sylvie Boldo and
Thi Minh Tuyen Nguyen},
editor = {C{\'{e}}sar A. Mu{\~{n}}oz},
title = {Hardware-independent Proofs of Numerical Programs},
booktitle = {Second {NASA} Formal Methods Symposium - {NFM} 2010, Washington D.C.,
USA, April 13-15, 2010. Proceedings},
series = {{NASA} Conference Proceedings},
volume = {{NASA/CP-2010-216215}},
pages = {14--23},
year = {2010},
timestamp = {Thu, 23 Jun 2016 15:53:27 +0200},
biburl = {https://dblp.org/rec/conf/nfm/BoldoN10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1005-0824,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Jean{-}Christophe Filli{\^{a}}tre and
Micaela Mayero and
Guillaume Melquiond and
Pierre Weis},
title = {Formal Proof of a Wave Equation Resolution Scheme: the Method Error},
journal = {CoRR},
volume = {abs/1005.0824},
year = {2010},
url = {http://arxiv.org/abs/1005.0824},
eprinttype = {arXiv},
eprint = {1005.0824},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1005-0824.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tc/Boldo09,
author = {Sylvie Boldo},
title = {Kahan's Algorithm for a Correct Discriminant Computation at Last Formally
Proven},
journal = {{IEEE} Trans. Computers},
volume = {58},
number = {2},
pages = {220--225},
year = {2009},
url = {https://doi.org/10.1109/TC.2008.200},
doi = {10.1109/TC.2008.200},
timestamp = {Sat, 20 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tc/Boldo09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tc/BoldoDL09,
author = {Sylvie Boldo and
Marc Daumas and
Ren{-}Cang Li},
title = {Formally Verified Argument Reduction with a Fused Multiply-Add},
journal = {{IEEE} Trans. Computers},
volume = {58},
number = {8},
pages = {1139--1145},
year = {2009},
url = {https://doi.org/10.1109/TC.2008.216},
doi = {10.1109/TC.2008.216},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tc/BoldoDL09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icalp/Boldo09,
author = {Sylvie Boldo},
editor = {Susanne Albers and
Alberto Marchetti{-}Spaccamela and
Yossi Matias and
Sotiris E. Nikoletseas and
Wolfgang Thomas},
title = {Floats and Ropes: {A} Case Study for Formal Numerical Program Verification},
booktitle = {Automata, Languages and Programming, 36th Internatilonal Colloquium,
{ICALP} 2009, Rhodes, Greece, July 5-12, 2009, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {5556},
pages = {91--102},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02930-1\_8},
doi = {10.1007/978-3-642-02930-1\_8},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/icalp/Boldo09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/BoldoFM09,
author = {Sylvie Boldo and
Jean{-}Christophe Filli{\^{a}}tre and
Guillaume Melquiond},
editor = {Jacques Carette and
Lucas Dixon and
Claudio Sacerdoti Coen and
Stephen M. Watt},
title = {Combining Coq and Gappa for Certifying Floating-Point Programs},
booktitle = {Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009,
8th International Conference, {MKM} 2009, Held as Part of {CICM} 2009,
Grand Bend, Canada, July 6-12, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5625},
pages = {59--74},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02614-0\_10},
doi = {10.1007/978-3-642-02614-0\_10},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/mkm/BoldoFM09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tc/BoldoM08,
author = {Sylvie Boldo and
Guillaume Melquiond},
title = {Emulation of a {FMA} and Correctly Rounded Sums: Proved Algorithms
Using Rounding to Odd},
journal = {{IEEE} Trans. Computers},
volume = {57},
number = {4},
pages = {462--471},
year = {2008},
url = {https://doi.org/10.1109/TC.2007.70819},
doi = {10.1109/TC.2007.70819},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tc/BoldoM08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoF07,
author = {Sylvie Boldo and
Jean{-}Christophe Filli{\^{a}}tre},
title = {Formal Verification of Floating-Point Programs},
booktitle = {18th {IEEE} Symposium on Computer Arithmetic {(ARITH-18} 2007), 25-27
June 2007, Montpellier, France},
pages = {187--194},
publisher = {{IEEE} Computer Society},
year = {2007},
url = {https://doi.org/10.1109/ARITH.2007.20},
doi = {10.1109/ARITH.2007.20},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/BoldoF07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0708-3722,
author = {Sylvie Boldo and
Marc Daumas and
Ren{-}Cang Li},
title = {Formally Verified Argument Reduction with a Fused-Multiply-Add},
journal = {CoRR},
volume = {abs/0708.3722},
year = {2007},
url = {http://arxiv.org/abs/0708.3722},
eprinttype = {arXiv},
eprint = {0708.3722},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0708-3722.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Boldo06,
author = {Sylvie Boldo},
editor = {Ulrich Furbach and
Natarajan Shankar},
title = {Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof
of the Veltkamp/Dekker Algorithms},
booktitle = {Automated Reasoning, Third International Joint Conference, {IJCAR}
2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4130},
pages = {52--66},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11814771\_6},
doi = {10.1007/11814771\_6},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Boldo06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sac/BoldoM06,
author = {Sylvie Boldo and
C{\'{e}}sar A. Mu{\~{n}}oz},
editor = {Hisham Haddad},
title = {Provably faithful evaluation of polynomials},
booktitle = {Proceedings of the 2006 {ACM} Symposium on Applied Computing (SAC),
Dijon, France, April 23-27, 2006},
pages = {1328--1332},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1141277.1141586},
doi = {10.1145/1141277.1141586},
timestamp = {Tue, 06 Nov 2018 11:06:49 +0100},
biburl = {https://dblp.org/rec/conf/sac/BoldoM06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoM05,
author = {Sylvie Boldo and
Jean{-}Michel Muller},
title = {Some Functions Computable with a Fused-Mac},
booktitle = {17th {IEEE} Symposium on Computer Arithmetic {(ARITH-17} 2005), 27-29
June 2005, Cape Cod, MA, {USA}},
pages = {52--58},
publisher = {{IEEE} Computer Society},
year = {2005},
url = {https://doi.org/10.1109/ARITH.2005.39},
doi = {10.1109/ARITH.2005.39},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/BoldoM05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/na/BoldoD04,
author = {Sylvie Boldo and
Marc Daumas},
title = {A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials},
journal = {Numer. Algorithms},
volume = {37},
number = {1-4},
pages = {45--60},
year = {2004},
url = {https://doi.org/10.1023/B:NUMA.0000049487.98618.61},
doi = {10.1023/B:NUMA.0000049487.98618.61},
timestamp = {Sat, 25 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/na/BoldoD04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sttt/BoldoD04,
author = {Sylvie Boldo and
Marc Daumas},
title = {Properties of two's complement floating point notations},
journal = {Int. J. Softw. Tools Technol. Transf.},
volume = {5},
number = {2-3},
pages = {237--246},
year = {2004},
url = {https://doi.org/10.1007/s10009-003-0120-y},
doi = {10.1007/S10009-003-0120-Y},
timestamp = {Thu, 02 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sttt/BoldoD04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BoldoD03,
author = {Sylvie Boldo and
Marc Daumas},
title = {Representable Correcting Terms for Possibly Underflowing Floating
Point Operations},
booktitle = {16th {IEEE} Symposium on Computer Arithmetic (Arith-16 2003), 15-18
June 2003, Santiago de Compostela, Spain},
pages = {79--86},
publisher = {{IEEE} Computer Society},
year = {2003},
url = {https://doi.org/10.1109/ARITH.2003.1207663},
doi = {10.1109/ARITH.2003.1207663},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/BoldoD03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/LiBD03,
author = {Ren{-}Cang Li and
Sylvie Boldo and
Marc Daumas},
title = {Theorems on Efficient Argument Reductions},
booktitle = {16th {IEEE} Symposium on Computer Arithmetic (Arith-16 2003), 15-18
June 2003, Santiago de Compostela, Spain},
pages = {129--136},
publisher = {{IEEE} Computer Society},
year = {2003},
url = {https://doi.org/10.1109/ARITH.2003.1207670},
doi = {10.1109/ARITH.2003.1207670},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arith/LiBD03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/BoldoD02,
author = {Sylvie Boldo and
Marc Daumas},
editor = {Rance Cleaveland and
Hubert Garavel},
title = {Properties of the subtraction valid for any floating point system},
booktitle = {7th International {ERCIM} Workshop in Formal Methods for Industrial
Critical Systems, {FMICS} 2002, {ICALP} 2002 Satellite Workshop, M{\'{a}}laga,
Spain, July 12-13, 2002},
series = {Electronic Notes in Theoretical Computer Science},
volume = {66},
number = {2},
pages = {132--144},
publisher = {Elsevier},
year = {2002},
url = {https://doi.org/10.1016/S1571-0661(04)80408-0},
doi = {10.1016/S1571-0661(04)80408-0},
timestamp = {Tue, 06 Dec 2022 10:27:25 +0100},
biburl = {https://dblp.org/rec/journals/entcs/BoldoD02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/cs-MS-0107025,
author = {Sylvie Boldo and
Marc Daumas and
Claire Moreau{-}Finot and
Laurent Th{\'{e}}ry},
title = {Computer validated proofs of a toolset for adaptable arithmetic},
journal = {CoRR},
volume = {cs.MS/0107025},
year = {2001},
url = {https://arxiv.org/abs/cs/0107025},
timestamp = {Fri, 10 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/cs-MS-0107025.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-04-21 18:01 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
