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-00135090v3  Conference papers
Sylvie BoldoMarc DaumasPascal 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-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-01350225v1  Journal articles
Sylvie Boldo. Un algorithme de découpe de gâteau
Interstices, INRIA, 2010
hal-01350274v1  Journal articles
Sylvie Boldo. Demandez le programme
Interstices, INRIA, 2009
hal-00157268v1  Journal articles
Sylvie BoldoMarc 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⟩
inria-00080427v2  Journal articles
Sylvie BoldoGuillaume 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⟩
hal-00712938v2  Conference papers
Sylvie BoldoCatherine LelayGuillaume 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⟩
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⟩
hal-00755333v1  Conference papers
Sylvie BoldoGuillaume 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
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⟩
hal-02101859v1  Reports
Sylvie BoldoJean-Michel Muller. Some Functions Computable with a Fused-mac
[Research Report] LIP RR-2004-41, Laboratoire de l'informatique du parallélisme. 2004, 2+10p
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⟩