Skip to Main content Skip to Navigation


...
tel-00789543v1  Theses
Paolo Herms. 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
Nikolai KosmatovClaude MarchéYannick MoyJulien Signoles. 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
François BobotJean-Christophe FilliâtreClaude MarchéGuillaume MelquiondAndrei Paskevich. 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-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-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-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
...
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⟩
...
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-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-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-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⟩
...
hal-01581807v1  Conference papers
Sylvie BoldoFrançois ClémentFlorian FaissoleVincent MartinMicaela Mayero. 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