default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSylvie Boldo
Person information
- affiliation: Université Paris-Sud, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[i9]Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin:
Teaching Divisibility and Binomials with Coq. CoRR abs/2404.12676 (2024)- 2023
- [j20]Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller
:
Floating-point arithmetic. Acta Numer. 32: 203-290 (2023) - [c27]Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine:
A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. FM 2023: 39-55 - 2022
- [j19]Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero:
A Coq Formalization of Lebesgue Integration of Nonnegative Functions. J. Autom. Reason. 66(2): 175-213 (2022) - [j18]Louise Ben Salem-Knapp, Sylvie Boldo, William Weens:
Bounding the Round-Off Error of the Upwind Scheme for Advection. IEEE Trans. Emerg. Top. Comput. 10(3): 1253-1262 (2022) - [c26]Louise Ben Salem-Knapp, Sylvie Boldo, William Weens:
Bounding the Round-Off Error of the Upwind Scheme for Advection. ARITH 2022: 127 - [i8]Sylvie Boldo, François Clément, Louise Leclerc:
A Coq Formalization of the Bochner integral. CoRR abs/2201.03242 (2022) - [i7]Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine:
Lebesgue Induction and Tonelli's Theorem in Coq. CoRR abs/2202.05040 (2022) - 2021
- [j17]Sylvie Boldo, Christoph Quirin Lauter, Jean-Michel Muller:
Emulating Round-to-Nearest Ties-to-Zero "Augmented" Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic. IEEE Trans. Computers 70(7): 1046-1058 (2021) - [c25]Sylvie Boldo, Guillaume Melquiond:
Some Formal Tools for Computer Arithmetic: Flocq and Gappa. ARITH 2021: 111-114 - [i6]Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero:
A Coq Formalization of Lebesgue Integration of Nonnegative Functions. CoRR abs/2104.05256 (2021) - 2020
- [j16]Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq:
Optimal inverse projection of floating-point addition. Numer. Algorithms 83(3): 957-986 (2020) - [j15]Sylvie Boldo, Florian Faissole, Alexandre Chapoutot:
Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods. IEEE Trans. Computers 69(12): 1745-1756 (2020) - [c24]Sylvie Boldo, Diane Gallois-Wong, Thibault Hilaire:
A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm. ARITH 2020: 9-16
2010 – 2019
- 2019
- [e2]Naofumi Takagi, Sylvie Boldo, Martin Langhammer:
26th IEEE Symposium on Computer Arithmetic, ARITH 2019, Kyoto, Japan, June 10-12, 2019. IEEE 2019, ISBN 978-1-7281-3366-9 [contents] - 2018
- [c23]Sylvie Boldo, Florian Faissole, Vincent Tourneur:
A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. ARITH 2018: 69-75 - [c22]Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire:
A Coq Formalization of Digital Filters. CICM 2018: 87-103 - 2017
- [b2]Sylvie Boldo, Guillaume Melquiond:
Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System. ISTE Press 2017, ISBN 978-1-7854-8112-3, pp. I-XX, 1-306 - [j14]Sylvie Boldo, Stef Graillat, Jean-Michel Muller:
On the Robustness of the 2Sum and Fast2Sum Algorithms. ACM Trans. Math. Softw. 44(1): 4:1-4:14 (2017) - [c21]Sylvie Boldo, Florian Faissole, Alexandre Chapoutot:
Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. ARITH 2017: 82-89 - [c20]Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero:
A Coq formal proof of the LaxMilgram theorem. CPP 2017: 79-89 - [c19]Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu:
Formal Verification of a Floating-Point Expansion Renormalization Algorithm. ITP 2017: 98-113 - [e1]Alessandro Abate, Sylvie Boldo:
Numerical Software Verification - 10th International Workshop, NSV 2017, Heidelberg, Germany, July 22-23, 2017, Proceedings [collocated with CAV 2017]. Lecture Notes in Computer Science 10381, Springer 2017, ISBN 978-3-319-63500-2 [contents] - 2016
- [j13]Sylvie Boldo, Catherine Lelay, Guillaume Melquiond:
Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7): 1196-1233 (2016) - [c18]Sylvie Boldo:
Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest. NSV@CAV 2016: 47-51 - 2015
- [j12]Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond:
Verified Compilation of Floating-Point Computations. J. Autom. Reason. 54(2): 135-163 (2015) - [j11]Sylvie Boldo, Catherine Lelay, Guillaume Melquiond:
Coquelicot: A User-Friendly Library of Real Analysis for Coq. Math. Comput. Sci. 9(1): 41-62 (2015) - [c17]Sylvie Boldo:
Formal Verification of Programs Computing the Floating-Point Average. ICFEM 2015: 17-32 - 2014
- [b1]Sylvie Boldo:
Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. University of Paris-Sud, Orsay, France, 2014 - [j10]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68(3): 325-352 (2014) - [c16]Sylvie Boldo:
Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number. NSV 2014: 27-32 - 2013
- [j9]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. 50(4): 423-456 (2013) - [c15]Sylvie Boldo:
How to Compute the Area of a Triangle: A Formal Revisit. IEEE Symposium on Computer Arithmetic 2013: 91-98 - [c14]Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond:
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic 2013: 107-115 - 2012
- [c13]Sylvie Boldo, Catherine Lelay, Guillaume Melquiond:
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. CPP 2012: 289-304 - [i5]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. CoRR abs/1212.6641 (2012) - 2011
- [j8]Sylvie Boldo, Thi Minh Tuyen Nguyen:
Proofs of numerical programs when the compiler optimizes. Innov. Syst. Softw. Eng. 7(2): 151-160 (2011) - [j7]Sylvie Boldo, Claude Marché:
Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs. Math. Comput. Sci. 5(4): 377-393 (2011) - [j6]Sylvie Boldo, Jean-Michel Muller:
Exact and Approximated Error of the FMA. IEEE Trans. Computers 60(2): 157-164 (2011) - [c12]Sylvie Boldo, Guillaume Melquiond:
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. IEEE Symposium on Computer Arithmetic 2011: 243-252 - [i4]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Wave Equation Numerical Resolution: Mathematics and Program. CoRR abs/1112.1795 (2011) - 2010
- [c11]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP 2010: 147-162 - [c10]Sylvie Boldo, Thi Minh Tuyen Nguyen:
Hardware-independent Proofs of Numerical Programs. NASA Formal Methods 2010: 14-23 - [i3]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Formal Proof of a Wave Equation Resolution Scheme: the Method Error. CoRR abs/1005.0824 (2010)
2000 – 2009
- 2009
- [j5]Sylvie Boldo:
Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven. IEEE Trans. Computers 58(2): 220-225 (2009) - [j4]Sylvie Boldo, Marc Daumas, Ren-Cang Li:
Formally Verified Argument Reduction with a Fused Multiply-Add. IEEE Trans. Computers 58(8): 1139-1145 (2009) - [c9]Sylvie Boldo:
Floats and Ropes: A Case Study for Formal Numerical Program Verification. ICALP (2) 2009: 91-102 - [c8]Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond:
Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus/MKM 2009: 59-74 - 2008
- [j3]Sylvie Boldo, Guillaume Melquiond:
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Trans. Computers 57(4): 462-471 (2008) - 2007
- [c7]Sylvie Boldo, Jean-Christophe Filliâtre:
Formal Verification of Floating-Point Programs. IEEE Symposium on Computer Arithmetic 2007: 187-194 - [i2]Sylvie Boldo, Marc Daumas, Ren-Cang Li:
Formally Verified Argument Reduction with a Fused-Multiply-Add. CoRR abs/0708.3722 (2007) - 2006
- [c6]Sylvie Boldo:
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. IJCAR 2006: 52-66 - [c5]Sylvie Boldo, César A. Muñoz:
Provably faithful evaluation of polynomials. SAC 2006: 1328-1332 - 2005
- [c4]Sylvie Boldo, Jean-Michel Muller:
Some Functions Computable with a Fused-Mac. IEEE Symposium on Computer Arithmetic 2005: 52-58 - 2004
- [j2]Sylvie Boldo, Marc Daumas:
A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials. Numer. Algorithms 37(1-4): 45-60 (2004) - [j1]Sylvie Boldo, Marc Daumas:
Properties of two's complement floating point notations. Int. J. Softw. Tools Technol. Transf. 5(2-3): 237-246 (2004) - 2003
- [c3]Sylvie Boldo, Marc Daumas:
Representable Correcting Terms for Possibly Underflowing Floating Point Operations. IEEE Symposium on Computer Arithmetic 2003: 79-86 - [c2]Ren-Cang Li, Sylvie Boldo, Marc Daumas:
Theorems on Efficient Argument Reductions. IEEE Symposium on Computer Arithmetic 2003: 129-136 - 2002
- [c1]Sylvie Boldo, Marc Daumas:
Properties of the subtraction valid for any floating point system. FMICS 2002: 132-144 - 2001
- [i1]Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Théry:
Computer validated proofs of a toolset for adaptable arithmetic. CoRR cs.MS/0107025 (2001)
Coauthor Index
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.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-05 20:23 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:
