Accéder directement au contenu

Sylvie Boldo

77
Documents
Identifiants chercheurs

Présentation

Auto-magically brought to you by HAL.
Auto-magically brought to you by HAL.

Publications

Même les ordinateurs font des erreurs !

Sylvie Boldo
Martin Andler; Liliane Bel; Sylvie Benzoni-Gavage; Thierry Goudon; Cyril Imbert; Antoine Rousseau. Brèves de maths, Nouveau Monde Editions, pp.136-137, 2014, 978-2-36583-896-2
Chapitre d'ouvrage hal-01089095v1

Arithmétique des ordinateurs et preuves formelles

Sylvie Boldo , Guillaume Melquiond
Informatique mathématique : Une photographie en 2013, 2013
Chapitre d'ouvrage hal-01767900v1
Image document

Floating-point arithmetic

Sylvie Boldo , Claude-Pierre Jeannerod , Guillaume Melquiond , Jean-Michel Muller
Acta Numerica, 2023, 32, pp.203-290. ⟨10.1017/S0962492922000101⟩
Article dans une revue hal-04095151v1

Le dilemme du fabricant de tables

Sylvie Boldo , Nicolas Brisebarre , Jean-Michel Muller
La Recherche, 2023, 572
Article dans une revue hal-03932037v1
Image document

Bounding the Round-Off Error of the Upwind Scheme for Advection

Louise Ben Salem-Knapp , Sylvie Boldo , William Weens
IEEE Transactions on Emerging Topics in Computing, 2022, 10 (3), ⟨10.1109/TETC.2022.3191472⟩
Article dans une revue hal-03329933v1
Image document

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero
Journal of Automated Reasoning, 2022, 66, pp.175-213. ⟨10.1007/s10817-021-09612-0⟩
Article dans une revue hal-03471095v1
Image document

Emulating round-to-nearest ties-to-zero "augmented" floating-point operations using round-to-nearest ties-to-even arithmetic

Sylvie Boldo , Christoph Q. Lauter , Jean-Michel Muller
IEEE Transactions on Computers, 2021, 70 (7), pp.1046 - 1058. ⟨10.1109/TC.2020.3002702⟩
Article dans une revue hal-02137968v4
Image document

Optimal Inverse Projection of Floating-Point Addition

Diane Gallois-Wong , Sylvie Boldo , Pascal Cuoq
Numerical Algorithms, In press, 83 (3), pp.957--986. ⟨10.1007/s11075-019-00711-z⟩
Article dans une revue hal-01939097v1
Image document

Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods

Sylvie Boldo , Florian Faissole , Alexandre Chapoutot
IEEE Transactions on Computers, 2019, ⟨10.1109/TC.2019.2917902⟩
Article dans une revue hal-01883843v3
Image document

On the robustness of the 2Sum and Fast2Sum algorithms

Sylvie Boldo , Stef Graillat , Jean-Michel Muller
ACM Transactions on Mathematical Software, 2017, 44 (1)
Article dans une revue ensl-01310023v2
Image document

Formalization of Real Analysis: A Survey of Proof Assistants and Libraries

Sylvie Boldo , Catherine Lelay , Guillaume Melquiond
Mathematical Structures in Computer Science, 2016, 26 (7), pp.1196-1233. ⟨10.1017/S0960129514000437⟩
Article dans une revue hal-00806920v2
Image document

Coquelicot: A User-Friendly Library of Real Analysis for Coq

Sylvie Boldo , Catherine Lelay , Guillaume Melquiond
Mathematics in Computer Science, 2015, 9 (1), pp.41-62. ⟨10.1007/s11786-014-0181-1⟩
Article dans une revue hal-00860648v2
Image document

Verified Compilation of Floating-Point Computations

Sylvie Boldo , Jacques-Henri Jourdan , Xavier Leroy , Guillaume Melquiond
Journal of Automated Reasoning, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩
Article dans une revue hal-00862689v3

Des ordinateurs capables de calculer plus juste

Jean-Michel Muller , Sylvie Boldo
La Recherche, 2014, pp.46-53
Article dans une revue ensl-01069744v1
Image document

Trusting computations: a mechanized proof from partial differential equations to actual program

Sylvie Boldo , François Clément , Jean-Christophe Filliâtre , Micaela Mayero , Guillaume Melquiond
Computers & Mathematics with Applications, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩
Article dans une revue hal-00769201v3
Image document

Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Sylvie Boldo , François Clément , Jean-Christophe Filliâtre , Micaela Mayero , Guillaume Melquiond
Journal of Automated Reasoning, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩
Article dans une revue hal-00649240v3
Image document

Exact and Approximated error of the FMA

Sylvie Boldo , Jean-Michel Muller
IEEE Transactions on Computers, 2011, 60 (2), pp.157-164. ⟨10.1109/TC.2010.139⟩
Article dans une revue inria-00429617v1
Image document

Proofs of numerical programs when the compiler optimizes

Sylvie Boldo , Thi Minh Tuyen Nguyen
Innovations in Systems and Software Engineering, 2011, 7, pp.151-160
Article dans une revue hal-00777639v1
Image document

Formal verification of numerical programs: from C annotated programs to mechanical proofs

Sylvie Boldo , Claude Marché
Mathematics in Computer Science, 2011, 5, pp.377-393
Article dans une revue hal-00777605v1

C'est la faute à l'ordinateur !

Sylvie Boldo
Interstices, 2010
Article dans une revue inria-00534848v1

Un algorithme de découpe de gâteau

Sylvie Boldo
Interstices, 2010
Article dans une revue hal-01350225v1
Image document

Kahan's algorithm for a correct discriminant computation at last formally proven

Sylvie Boldo
IEEE Transactions on Computers, 2009, 58 (2), pp.220-225. ⟨10.1109/TC.2008.200⟩
Article dans une revue inria-00171497v2

Demandez le programme

Sylvie Boldo
Interstices, 2009
Article dans une revue hal-01350274v1
Image document

Computing predecessor and successor in rounding to nearest

Siegfried Rump , Paul Zimmermann , Sylvie Boldo , Guillaume Melquiond
BIT Numerical Mathematics, 2009, 49 (2), pp.419-431. ⟨10.1007/s10543-009-0218-z⟩
Article dans une revue inria-00337537v1
Image document

Formally Verified Argument Reduction with a Fused Multiply-Add

Sylvie Boldo , Marc Daumas , Ren-Cang Li
IEEE Transactions on Computers, 2009, 58 (8), pp.1139-1145. ⟨10.1109/TC.2008.216⟩
Article dans une revue hal-00168401v2

Floats & Ropes: a case study for formal numerical program verification

Sylvie Boldo
Lecture Notes in Computer Science, 2009, 36th International Colloquium on Automata, Languages and Programming, 5556, pp.91--102. ⟨10.1007/978-3-642-02930-1_8⟩
Article dans une revue inria-00432718v1
Image document

Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd

Sylvie Boldo , Guillaume Melquiond
IEEE Transactions on Computers, 2008, 57 (4), pp.462-471. ⟨10.1109/TC.2007.70819⟩
Article dans une revue inria-00080427v2

Idée reçue : L’informatique, ce n’est pas pour les filles

Sylvie Boldo , Thierry Viéville
Interstices, 2008
Article dans une revue hal-01350416v1

Pourquoi mon ordinateur calcule-t-il faux ?

Sylvie Boldo , Joanna Jongwane
Interstices, 2008
Article dans une revue hal-01350419v1
Image document

A simple test qualifying the accuracy of Horner's rule for polynomials

Sylvie Boldo , Marc Daumas
Numerical Algorithms, 2004, 37 (1-4), pp.45-60. ⟨10.1023/B:NUMA.0000049487.98618.61⟩
Article dans une revue inria-00071879v1
Image document

Properties of two's complement floating point notations

Sylvie Boldo , Marc Daumas
International Journal on Software Tools for Technology Transfer, 2003, 5 (2-3), pp.237-246. ⟨10.1007/s10009-003-0120-y⟩
Article dans une revue hal-00157268v1
Image document

A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem

Sylvie Boldo , François Clément , Vincent Martin , Micaela Mayero , Houda Mouhcine
25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.39--55, ⟨10.1007/978-3-031-27481-7_4⟩
Communication dans un congrès hal-03889276v2
Image document

Some Formal Tools for Computer Arithmetic: Flocq and Gappa

Sylvie Boldo , Guillaume Melquiond
ARITH 2021 - 28th IEEE International Symposium on Computer Arithmetic, Jun 2021, Online, Italy
Communication dans un congrès hal-03233227v1
Image document

A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm

Sylvie Boldo , Diane Gallois-Wong , Thibault Hilaire
ARITH 2020 - IEEE 27th Symposium on Computer Arithmetic, Jun 2020, Portland, United States. pp.9-16, ⟨10.1109/ARITH48897.2020.00011⟩
Communication dans un congrès hal-02982017v1
Image document

A Coq formalization of digital filters

Diane Gallois-Wong , Sylvie Boldo , Thibault Hilaire
CICM 2018 - 11th Conference on Intelligent Computer Mathematics, Aug 2018, Hagenberg, Austria. pp.87--103, ⟨10.1007/978-3-319-96812-4_8⟩
Communication dans un congrès hal-01728828v2
Image document

A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers

Sylvie Boldo , Florian Faissole , Vincent Tourneur
25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States
Communication dans un congrès hal-01772272v1
Image document

Round-off Error Analysis of Explicit One-Step Numerical Integration Methods

Sylvie Boldo , Florian Faissole , Alexandre Chapoutot
24th IEEE Symposium on Computer Arithmetic, Jul 2017, London, United Kingdom. ⟨10.1109/ARITH.2017.22⟩
Communication dans un congrès hal-01581794v1
Image document

Formal Verification of a Floating-Point Expansion Renormalization Algorithm

Sylvie Boldo , Mioara Joldes , Jean-Michel Muller , Valentina Popescu
8th International Conference on Interactive Theorem Proving (ITP'2017), Sep 2017, Brasilia, Brazil
Communication dans un congrès hal-01512417v1
Image document

Preuve formelle du théorème de Lax–Milgram

Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero
16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France
Communication dans un congrès hal-01581807v1
Image document

A Coq formal proof of the Lax–Milgram theorem

Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero
6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩
Communication dans un congrès hal-01391578v1
Image document

Iterators: where folds fail

Sylvie Boldo
Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada
Communication dans un congrès hal-01377155v1
Image document

Computing a correct and tight rounding error bound using rounding-to-nearest

Sylvie Boldo
9th International Workshop on Numerical Software Verification, Jul 2016, Toronto, Canada
Communication dans un congrès hal-01377152v1
Image document

Formal Verification of Programs Computing the Floating-Point Average

Sylvie Boldo
17th International Conference on Formal Engineering Methods, Nov 2015, Paris, France. pp.17-32
Communication dans un congrès hal-01174892v1
Image document

Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number

Sylvie Boldo
Seventh and Eighth International Workshop on Numerical Software Verification, Apr 2015, Seattle, WA, United States. pp.50--55
Communication dans un congrès hal-01148409v1
Image document

Formal verification of tricky numerical computations

Sylvie Boldo
16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Sep 2014, Würzburg, Germany. pp.39
Communication dans un congrès hal-01088692v1
Image document

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic

Sylvie Boldo , Jacques-Henri Jourdan , Xavier Leroy , Guillaume Melquiond
Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115
Communication dans un congrès hal-00743090v2
Image document

How to Compute the Area of a Triangle: a Formal Revisit

Sylvie Boldo
21st IEEE International Symposium on Computer Arithmetic, Apr 2013, Austin, TX, United States. pp.91-98, ⟨10.1109/ARITH.2013.29⟩
Communication dans un congrès hal-00790071v1
Image document

Arithmétique des ordinateurs et preuves formelles

Sylvie Boldo , Guillaume Melquiond
École des Jeunes Chercheurs en Informatique Mathématique, GDR Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30
Communication dans un congrès hal-00755333v1
Image document

Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives

Sylvie Boldo , Catherine Lelay , Guillaume Melquiond
CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. pp.289-304, ⟨10.1007/978-3-642-35308-6_22⟩
Communication dans un congrès hal-00712938v2
Image document

Flocq: A Unified Library for Proving Floating-point Algorithms in Coq

Sylvie Boldo , Guillaume Melquiond
Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Jul 2011, Tübingen, Germany. pp.243-252, ⟨10.1109/ARITH.2011.40⟩
Communication dans un congrès inria-00534854v2
Image document

Formal proof of a wave equation resolution scheme: the method error

Sylvie Boldo , François Clément , Jean-Christophe Filliâtre , Micaela Mayero , Guillaume Melquiond
ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.147-162, ⟨10.1007/978-3-642-14052-5_12⟩
Communication dans un congrès inria-00450789v3
Image document

Formal verification of numerical programs: from C annotated programs to Coq proofs

Sylvie Boldo
NSV-3: Third International Workshop on Numerical Software Verification, Jul 2010, Edinburgh, Scotland, United Kingdom
Communication dans un congrès inria-00534400v1
Image document

Hardware-independent proofs of numerical programs

Sylvie Boldo , Thi Minh Tuyen Nguyen
Second NASA Formal Methods Symposium (NFM 2010), NASA, Apr 2010, Washington D.C., United States. pp.14-23
Communication dans un congrès inria-00534410v1
Image document

Combining Coq and Gappa for Certifying Floating-Point Programs

Sylvie Boldo , Jean-Christophe Filliâtre , Guillaume Melquiond
16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. pp.59-74, ⟨10.1007/978-3-642-02614-0_10⟩
Communication dans un congrès inria-00432726v1
Image document

Formal proof for delayed finite field arithmetic using floating point operators

Sylvie Boldo , Marc Daumas , Pascal Giorgi
8th Conference on Real Numbers and Computers, Jul 2008, Saint Jacques de Compostelle, Spain. pp.113-122
Communication dans un congrès hal-00135090v3
Image document

Provably Faithful Evaluation of Polynomials

Sylvie Boldo , César Muñoz
21st Annual ACM Symposium on Applied Computing, Apr 2006, Dijon, France
Communication dans un congrès inria-00000892v1
Image document

When double rounding is odd

Sylvie Boldo , Guillaume Melquiond
17th IMACS World Congress, Jul 2005, Paris, France. pp.11
Communication dans un congrès inria-00070603v2
Image document

Some Functions Computable with a Fused-mac

Sylvie Boldo , Jean-Michel Muller
17th IEEE Symposium on Computer Arithmetic, Jun 2005, Cape Cod, Massachusetts, USA, pp.52-58
Communication dans un congrès inria-00000895v1
Image document

Theorems on Efficient Argument Reductions

Ren Cang Li , Sylvie Boldo , Marc Daumas
16th IEEE Symposium on Computer Arithmetic, 2003, Santiago de Compostela, Spain. pp.129-136, ⟨10.1109/ARITH.2003.1207670⟩
Communication dans un congrès hal-00156244v1
Image document

Properties of the subtraction valid for any floating point system

Sylvie Boldo , Marc Daumas
7th International Workshop on Formal Methods for Industrial Critical Systems, 2002, Málaga, Spain. pp.137-149
Communication dans un congrès inria-00072115v1
Image document

Formal proofs of numerical programs

Nguyen Thi Minh Tuyen , Sylvie Boldo , Claude Marché
Forum Digitéo, Oct 2010, Palaiseau, France
Poster de conférence inria-00536135v1
Image document

Lebesgue Induction and Tonelli's Theorem in Coq

Sylvie Boldo , François Clément , Vincent Martin , Micaela Mayero , Houda Mouhcine
[Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2023, pp.17
Rapport hal-03564379v2
Image document

A Coq Formalization of the Bochner integral

Sylvie Boldo , François Clément , Louise Leclerc
[Research Report] RR-9456, Inria Saclay - Île de France; Inria de Paris. 2022
Rapport hal-03516749v2
Image document

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero
[Research Report] RR-9401, Inria, France. 2021, pp.38
Rapport hal-03194113v2
Image document

Médiation Scientifique : une facette de nos métiers de la recherche

Antoine Rousseau , Aurélie Darnaud , Brice Goglin , Céline Acharian , Christine Leininger
[Interne] Inria. 2013, pp.34
Rapport hal-00804915v1
Image document

When double rounding is odd

Sylvie Boldo , Guillaume Melquiond
[Research Report] LIP RR-2004-48, Laboratoire de l'informatique du parallélisme. 2004, 2+7p
Rapport hal-02101979v1
Image document

Some Functions Computable with a Fused-mac

Sylvie Boldo , Jean-Michel Muller
[Research Report] LIP RR-2004-41, Laboratoire de l'informatique du parallélisme. 2004, 2+10p
Rapport hal-02101859v1
Image document

A simple test qualifying the accuracy of Horner's rule for polynomials

Sylvie Boldo , Marc Daumas
[Research Report] LIP RR-2003-01, Laboratoire de l'informatique du parallélisme. 2003, 2+39p
Rapport hal-02102015v1
Image document

Necessary and sufficient conditions for exact floating point operations

Marc Daumas , Sylvie Boldo
[Research Report] RR-4644, LIP RR-2002-44, INRIA, LIP. 2002
Rapport inria-00071941v1