Skip to Main content Skip to Navigation


...
ensl-00117386v1  Conference papers
Jérémie DetreyFlorent de DinechinXavier Pujol. Return of the hardware floating-point elementary function
18th Symposium on Computer Arithmetic, Jun 2007, Montpellier, France. pp.161-168
...
ensl-00269219v1  Conference papers
Nicolas BrisebarreFlorent de DinechinJean-Michel Muller. Integer and Floating-Point Constant Multipliers for FPGAs
International Conference on Application-Specific Systems, Architectures and Processors, 2008, IMEC, Jul 2008, Leuven, Belgium. pp.239-244, ⟨10.1109/ASAP.2008.4580184⟩
...
tel-00460776v5  Theses
Sylvain Chevillard. Évaluation efficace de fonctions numériques - Outils et exemples
Modélisation et simulation. Université de Lyon; Ecole Normale Supérieure de Lyon - ENS LYON, 2009. Français
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-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-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-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⟩
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
...
hal-00743090v2  Conference papers
Sylvie BoldoJacques-Henri JourdanXavier LeroyGuillaume 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-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⟩