 |
 |
 |
|
|
||
|---|---|---|
| hal-01783851v1
Preprints, Working Papers, ...
A Toolchain to Produce Correct-by-Construction OCaml Programs 2018 |
||
| tel-00789543v1
Theses
Certification of a Tool Chain for Deductive Program Verification Other [cs.OH]. Université Paris Sud - Paris XI, 2013. English. ⟨NNT : 2013PA112006⟩ |
||
| hal-01344110v1
Conference papers
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014 7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. pp.461--478 |
||
| hal-00875395v1
Conference papers
Preserving User Proofs Across Specification Changes Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201 |
||
| 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 |
||
| 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-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-01405762v1
Conference papers
Synthetic topology in HoTT for probabilistic programming The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Jan 2017, Paris, France |
||
| 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⟩ |
||
| 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-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-00743090v2
Conference papers
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-01391578v1
Conference papers
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-00769201v3
Journal articles
Trusting computations: a mechanized proof from partial differential equations to actual program Computers & Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩ |
||
| hal-01581807v1
Conference papers
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 |
||
|
|
||
