 |
 |
 |
|
|
||
|---|---|---|
| hal-00862653v1
Preprints, Working Papers, ...
How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound 2013 |
||
| hal-02433652v1
Directions of work or proceedings
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
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 |
||
| inria-00337537v1
Journal articles
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⟩ |
||
| hal-01350416v1
Journal articles
Idée reçue : L’informatique, ce n’est pas pour les filles Interstices, INRIA, 2008 |
||
| hal-01377155v1
Conference papers
Iterators: where folds fail Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada |
||
| hal-01707376v1
Directions of work or proceedings
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
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
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
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
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
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
10th International Workshop on Numerical Software Verification 10th International Workshop on Numerical Software Verification, France. Springer, 2017 |
||
| tel-01089643v1
Habilitation à diriger des recherches
Deductive Formal Verification: How To Make Your Floating-Point Programs Behave Computer Arithmetic. Université Paris-Sud, 2014 |
||
| hal-01148409v1
Conference papers
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-00860648v2
Journal articles
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-01089095v1
Book sections
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
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
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
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
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
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-00018530v1
Preprints, Working Papers, ...
Computer validated proofs of a toolset for adaptable arithmetic 2001  |
||
|
|
||
| hal-00862689v3
Journal articles
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
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
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⟩ |
||
|
|
||
