Skip to Main content

Keywords

Co-authors

Researcher identifiers

  • IdHAL : sboldo
Number of documents

67

CV of Sylvie Boldo


Auto-magically brought to you by HAL.


Books2 documents

  • Sylvie Boldo, Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press - Elsevier, pp.326, 2017, 9781785481123. ⟨hal-01632617⟩
  • Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Sylvie Boldo, Denis Bouhineau, et al.. Une introduction à la science informatique pour les enseignants de la discipline en lycée. Gilles Dowek. CRDP Paris, pp.376, 2011, Repères pour agir (RPA disciplines & compétences), Christine Moulin, 978-2-86631-188-9. ⟨hal-00765226⟩

Book sections2 documents

  • Sylvie Boldo. Même les ordinateurs font des erreurs !. 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. ⟨hal-01089095⟩
  • Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. Informatique mathématique : Une photographie en 2013, 2013. ⟨hal-01767900⟩

Directions of work or proceedings4 documents

  • Sylvie Boldo, Martin Langhammer. Proceedings of the 26th Symposium on Computer Arithmetic (ARITH 2019). ARITH 2019 - 26th IEEE Symposium on Computer Arithmetic, Jun 2019, Kyoto, IEEE, 2019, 978-1-7281-3367-6. ⟨10.1109/ARITH.2019.00005⟩. ⟨hal-02433652⟩
  • Sylvie Boldo, Nicolas Magaud. Journées Francophones des Langages Applicatifs 2018. Sylvie Boldo; Nicolas Magaud. Journées Francophones des Langages Applicatifs 2018, Jan 2018, Banyuls-sur-Mer, France. publié par les auteurs, 2018. ⟨hal-01707376⟩
  • Alessandro Abate, Sylvie Boldo. 10th International Workshop on Numerical Software Verification. 10th International Workshop on Numerical Software Verification, France. Springer, 2017. ⟨hal-01662076⟩
  • Sylvie Boldo, Julien Signoles. Vingt-huitièmes Journées Francophones des Langages Applicatifs. Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France. Published by the authors, 2017. ⟨hal-01662072⟩

Journal articles25 documents

  • Sylvie Boldo, Christoph Lauter, Jean-Michel Muller. Emulating round-to-nearest ties-to-zero "augmented" floating-point operations using round-to-nearest ties-to-even arithmetic. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, In press, ⟨10.1109/TC.2020.3002702⟩. ⟨hal-02137968v4⟩
  • Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq. Optimal Inverse Projection of Floating-Point Addition. Numerical Algorithms, Springer Verlag, In press, 83 (3), pp.957--986. ⟨10.1007/s11075-019-00711-z⟩. ⟨hal-01939097⟩
  • Sylvie Boldo, Florian Faissole, Alexandre Chapoutot. Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, In press, ⟨10.1109/TC.2019.2917902⟩. ⟨hal-01883843v3⟩
  • Sylvie Boldo, Stef Graillat, Jean-Michel Muller. On the robustness of the 2Sum and Fast2Sum algorithms. ACM Transactions on Mathematical Software, Association for Computing Machinery, 2017, 44 (1). ⟨ensl-01310023v2⟩
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Formalization of Real Analysis: A Survey of Proof Assistants and Libraries. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2016, 26 (7), pp.1196-1233. ⟨10.1017/S0960129514000437⟩. ⟨hal-00806920v2⟩
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science, Springer, 2015, 9 (1), pp.41-62. ⟨10.1007/s11786-014-0181-1⟩. ⟨hal-00860648v2⟩
  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩. ⟨hal-00862689v3⟩
  • Jean-Michel Muller, Sylvie Boldo. Des ordinateurs capables de calculer plus juste. La Recherche : l'actualité des sciences, société d'éditions scientifiques, 2014, pp.46-53. ⟨ensl-01069744⟩
  • Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Trusting computations: a mechanized proof from partial differential equations to actual program. Computers and Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩. ⟨hal-00769201v3⟩
  • Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, Springer Verlag, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩. ⟨hal-00649240v3⟩
  • Sylvie Boldo, Thi Minh Tuyen Nguyen. Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering, Springer Verlag, 2011, 7, pp.151-160. ⟨hal-00777639⟩
  • Sylvie Boldo, Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, Springer, 2011, 5, pp.377-393. ⟨hal-00777605⟩
  • Sylvie Boldo, Jean-Michel Muller. Exact and Approximated error of the FMA. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2011, 60 (2), pp.157-164. ⟨10.1109/TC.2010.139⟩. ⟨inria-00429617⟩
  • Sylvie Boldo. Un algorithme de découpe de gâteau. Interstices, INRIA, 2010. ⟨hal-01350225⟩
  • Sylvie Boldo. C'est la faute à l'ordinateur !. Interstices, INRIA, 2010. ⟨inria-00534848⟩
  • Sylvie Boldo. Demandez le programme. Interstices, INRIA, 2009. ⟨hal-01350274⟩
  • Sylvie Boldo, Marc Daumas, Ren-Cang Li. Formally Verified Argument Reduction with a Fused Multiply-Add. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2009, 58 (8), pp.1139-1145. ⟨10.1109/TC.2008.216⟩. ⟨hal-00168401v2⟩
  • Siegfried Rump, Paul Zimmermann, Sylvie Boldo, Guillaume Melquiond. Computing predecessor and successor in rounding to nearest. BIT Numerical Mathematics, Springer Verlag, 2009, 49 (2), pp.419-431. ⟨10.1007/s10543-009-0218-z⟩. ⟨inria-00337537⟩
  • Sylvie Boldo. Kahan's algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2009, 58 (2), pp.220-225. ⟨10.1109/TC.2008.200⟩. ⟨inria-00171497v2⟩
  • Sylvie Boldo. Floats & Ropes: a case study for formal numerical program verification. Lecture Notes in Computer Science, Springer, 2009, 36th International Colloquium on Automata, Languages and Programming, 5556, pp.91--102. ⟨10.1007/978-3-642-02930-1_8⟩. ⟨inria-00432718⟩
  • Sylvie Boldo, Thierry Viéville. Idée reçue : L’informatique, ce n’est pas pour les filles. Interstices, INRIA, 2008. ⟨hal-01350416⟩
  • Sylvie Boldo, Joanna Jongwane. Pourquoi mon ordinateur calcule-t-il faux ?. Interstices, INRIA, 2008. ⟨hal-01350419⟩
  • Sylvie Boldo, Guillaume Melquiond. Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2008, 57 (4), pp.462-471. ⟨10.1109/TC.2007.70819⟩. ⟨inria-00080427v2⟩
  • Sylvie Boldo, Marc Daumas. A simple test qualifying the accuracy of Horner's rule for polynomials. Numerical Algorithms, Springer Verlag, 2004, 37 (1-4), pp.45-60. ⟨10.1023/B:NUMA.0000049487.98618.61⟩. ⟨inria-00071879⟩
  • Sylvie Boldo, Marc Daumas. Properties of two's complement floating point notations. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2003, 5 (2-3), pp.237-246. ⟨10.1007/s10009-003-0120-y⟩. ⟨hal-00157268⟩

Conference papers26 documents

  • Sylvie Boldo, Diane Gallois-Wong, Thibault Hilaire. A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm. 2020 IEEE 27th Symposium on Computer Arithmetic (ARITH), Jun 2020, Portland, United States. pp.9-16, ⟨10.1109/ARITH48897.2020.00011⟩. ⟨hal-02982017⟩
  • Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire. A Coq formalization of digital filters. CICM 2018 - 11th Conference on Intelligent Computer Mathematics, Aug 2018, Hagenberg, Austria. pp.87--103, ⟨10.1007/978-3-319-96812-4_8⟩. ⟨hal-01728828v2⟩
  • Sylvie Boldo, Florian Faissole, Vincent Tourneur. A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. 25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States. ⟨hal-01772272⟩
  • Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. Preuve formelle du théorème de Lax–Milgram. 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France. ⟨hal-01581807⟩
  • Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu. Formal Verification of a Floating-Point Expansion Renormalization Algorithm. 8th International Conference on Interactive Theorem Proving (ITP'2017), Sep 2017, Brasilia, Brazil. ⟨hal-01512417⟩
  • Sylvie Boldo, Florian Faissole, Alexandre Chapoutot. Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. 24th IEEE Symposium on Computer Arithmetic, Jul 2017, London, United Kingdom. ⟨10.1109/ARITH.2017.22⟩. ⟨hal-01581794⟩
  • Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. A Coq formal proof of the Lax–Milgram theorem. 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩. ⟨hal-01391578⟩
  • Sylvie Boldo. Computing a correct and tight rounding error bound using rounding-to-nearest. 9th International Workshop on Numerical Software Verification, Jul 2016, Toronto, Canada. ⟨hal-01377152⟩
  • Sylvie Boldo. Iterators: where folds fail. Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada. ⟨hal-01377155⟩
  • Sylvie Boldo. Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number. Seventh and Eighth International Workshop on Numerical Software Verification, Apr 2015, Seattle, WA, United States. pp.50--55. ⟨hal-01148409⟩
  • Sylvie Boldo. Formal verification of tricky numerical computations. 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Sep 2014, Würzburg, Germany. pp.39. ⟨hal-01088692⟩
  • Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit. 21st IEEE International Symposium on Computer Arithmetic, Apr 2013, Austin, TX, United States. pp.91-98, ⟨10.1109/ARITH.2013.29⟩. ⟨hal-00790071⟩
  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115. ⟨hal-00743090v2⟩
  • Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. École des Jeunes Chercheurs en Informatique Mathématique, GDR Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30. ⟨hal-00755333⟩
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. 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⟩. ⟨hal-00712938v2⟩
  • Sylvie Boldo, Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-point Algorithms in Coq. Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Jul 2011, Tübingen, Germany. pp.243-252, ⟨10.1109/ARITH.2011.40⟩. ⟨inria-00534854v2⟩
  • Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Formal proof of a wave equation resolution scheme: the method error. ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.147-162, ⟨10.1007/978-3-642-14052-5_12⟩. ⟨inria-00450789v3⟩
  • Sylvie Boldo, Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. Second NASA Formal Methods Symposium (NFM 2010), NASA, Apr 2010, Washington D.C., United States. pp.14-23. ⟨inria-00534410⟩
  • Sylvie Boldo. Formal verification of numerical programs: from C annotated programs to Coq proofs. NSV-3: Third International Workshop on Numerical Software Verification, Jul 2010, Edinburgh, Scotland, United Kingdom. ⟨inria-00534400⟩
  • Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. 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⟩. ⟨inria-00432726⟩
  • Sylvie Boldo, Marc Daumas, Pascal Giorgi. Formal proof for delayed finite field arithmetic using floating point operators. 8th Conference on Real Numbers and Computers, Jul 2008, Saint Jacques de Compostelle, Spain. pp.113-122. ⟨hal-00135090v3⟩
  • Sylvie Boldo, César Muñoz. Provably Faithful Evaluation of Polynomials. 21st Annual ACM Symposium on Applied Computing, Apr 2006, Dijon, France. ⟨inria-00000892⟩
  • Sylvie Boldo, Guillaume Melquiond. When double rounding is odd. 17th IMACS World Congress, Jul 2005, Paris, France. pp.11. ⟨inria-00070603v2⟩
  • Sylvie Boldo, Jean-Michel Muller. Some Functions Computable with a Fused-mac. 17th IEEE Symposium on Computer Arithmetic, Jun 2005, Cape Cod, Massachusetts, USA, pp.52-58. ⟨inria-00000895⟩
  • Ren Cang Li, Sylvie Boldo, Marc Daumas. Theorems on Efficient Argument Reductions. 16th IEEE Symposium on Computer Arithmetic, 2003, Santiago de Compostela, Spain. pp.129-136, ⟨10.1109/ARITH.2003.1207670⟩. ⟨hal-00156244⟩
  • Sylvie Boldo, Marc Daumas. Properties of the subtraction valid for any floating point system. 7th International Workshop on Formal Methods for Industrial Critical Systems, 2002, Málaga, Spain. pp.137-149. ⟨inria-00072115⟩

Poster communications1 document

  • Nguyen Thi Minh Tuyen, Sylvie Boldo, Claude Marché. Formal proofs of numerical programs. Forum Digitéo, Oct 2010, Palaiseau, France. ⟨inria-00536135⟩

Other publications2 documents

  • Thierry Viéville, Sylvie Boldo, Florent Masseglia, Pierre Bernhard. « Structures : organisation, complexité, dynamique » des mot-clés au sens inattendu. 2015. ⟨hal-01238442⟩
  • Sylvie Boldo. L'informatique. 2010. ⟨inria-00534852⟩

Preprints, Working Papers, ...2 documents

  • Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound. 2013. ⟨hal-00862653⟩
  • Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Thery. Computer validated proofs of a toolset for adaptable arithmetic. 2001. ⟨hal-00018530⟩

Reports2 documents

  • Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, et al.. Médiation Scientifique : une facette de nos métiers de la recherche. [Interne] none. 2013, pp.34. ⟨hal-00804915⟩
  • Marc Daumas, Sylvie Boldo. Necessary and sufficient conditions for exact floating point operations. [Research Report] RR-4644, LIP RR-2002-44, INRIA, LIP. 2002. ⟨inria-00071941⟩

Habilitation à diriger des recherches1 document

  • Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Computer Arithmetic. Université Paris-Sud, 2014. ⟨tel-01089643⟩