Skip to Main content Skip to Navigation

hal-02433652v1  Directions of work or proceedings
Sylvie BoldoMartin 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-01088692v1  Conference papers
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-01377155v1  Conference papers
Sylvie Boldo. Iterators: where folds fail
Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada
hal-01707376v1  Directions of work or proceedings
Sylvie BoldoNicolas 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-01772272v1  Conference papers
Sylvie BoldoFlorian FaissoleVincent 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-00790071v1  Conference papers
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-01377152v1  Conference papers
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-01174892v1  Conference papers
Sylvie Boldo. Formal Verification of Programs Computing the Floating-Point Average
17th International Conference on Formal Engineering Methods, Nov 2015, Paris, France. pp.17-32
hal-01662076v1  Directions of work or proceedings
Alessandro AbateSylvie Boldo. 10th International Workshop on Numerical Software Verification
10th International Workshop on Numerical Software Verification, France. Springer, 2017
tel-01089643v1  Habilitation à diriger des recherches
Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave
Computer Arithmetic. Université Paris-Sud, 2014
hal-01148409v1  Conference papers
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-01089095v1  Book sections
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-01405762v1  Conference papers
Florian FaissoleBas Spitters. Synthetic topology in HoTT for probabilistic programming
The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Jan 2017, Paris, France
inria-00432718v1  Journal articles
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-00534852v1  Other publications
Sylvie Boldo. L'informatique
hal-00862689v3  Journal articles
Sylvie BoldoJacques-Henri JourdanXavier LeroyGuillaume 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⟩
inria-00429617v1  Journal articles
Sylvie BoldoJean-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⟩
hal-01391578v1  Conference papers
Sylvie BoldoFrançois ClémentFlorian FaissoleVincent MartinMicaela 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⟩
inria-00000892v1  Conference papers
Sylvie BoldoCésar Muñoz. Provably Faithful Evaluation of Polynomials
21st Annual ACM Symposium on Applied Computing, Apr 2006, Dijon, France
hal-02982017v1  Conference papers
Sylvie BoldoDiane Gallois-WongThibault Hilaire. A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm
ARITH 2020 - IEEE 27th Symposium on Computer Arithmetic, Jun 2020, Portland, United States. pp.9-16, ⟨10.1109/ARITH48897.2020.00011⟩
inria-00534854v2  Conference papers
Sylvie BoldoGuillaume 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-00000895v1  Conference papers
Sylvie BoldoJean-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-00536135v1  Poster communications
Nguyen Thi Minh TuyenSylvie BoldoClaude Marché. Formal proofs of numerical programs
Forum Digitéo, Oct 2010, Palaiseau, France
inria-00432726v1  Conference papers
Sylvie BoldoJean-Christophe FilliâtreGuillaume 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⟩
hal-01728828v2  Conference papers
Diane Gallois-WongSylvie BoldoThibault 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⟩
inria-00534410v1  Conference papers
Sylvie BoldoThi 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-00171497v2  Journal articles
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-00534848v1  Journal articles
Sylvie Boldo. C'est la faute à l'ordinateur !
Interstices, INRIA, 2010
inria-00534400v1  Conference papers
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