Mots-clés

Co-auteurs

Identifiants chercheur

  • IdHAL : sboldo
Nombre de documents

55

CV of Sylvie Boldo


Auto-magically brought to you by HAL.


Article dans une revue23 documents

Communication dans un congrès23 documents

  • Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. A Coq Formal Proof of the Lax–Milgram theorem. 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. 〈http://cpp2017.mpi-sws.org/〉. 〈10.1145/3018610.3018625〉. 〈hal-01391578〉
  • Sylvie Boldo, Florian Faissole, Alexandre Chapoutot. Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. 24th IEEE Symposium on Computer Arithmetic, Jul 2017, London, United Kingdom. 〈http://arith24.arithsymposium.org/〉. 〈10.1109/ARITH.2017.22〉. 〈hal-01581794〉
  • Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela 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. 〈http://afadl2017.imag.fr/〉. 〈hal-01581807〉
  • Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu. Formal Verification of a Floating-Point Expansion Renormalization Algorithm. 8th International Conference on Interactive Theorem Proving (ITP'2017), Sep 2017, Brasilia, Brazil. 2017, Proceedings of the 8th International Conference on Interactive Theorem Proving (ITP'2017). 〈hal-01512417〉
  • 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. 2016. 〈hal-01377152〉
  • Sylvie Boldo. Iterators: where folds fail. Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada. 〈hal-01377155〉
  • Sylvie Boldo. Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number. Sergiy Bogomolov and Matthieu Martel. Eighth International Workshop on Numerical Software Verification, Apr 2015, Seattle, WA, United States. Electronic Notes in Theoretical Computer Science, pp.50--55, 2015, Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification. 〈http://nsv2015.informatik.uni-freiburg.de/〉. 〈hal-01148409〉
  • Sylvie Boldo. Formal verification of tricky numerical computations. Marco Nehmeier. 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Sep 2014, Würzburg, Germany. pp.39, 2014, 〈http://www.scan2014.uni-wuerzburg.de/〉. 〈hal-01088692〉
  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. IEEE, pp.107-115, 2013. 〈hal-00743090v2〉
  • Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit. Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang. 21st IEEE International Symposium on Computer Arithmetic, Apr 2013, Austin, TX, United States. IEEE, pp.91-98, 2013, 〈10.1109/ARITH.2013.29〉. 〈hal-00790071〉
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. Chris Hawblitzel and Dale Miller. CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. Springer, 7679, pp.289-304, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35308-6_22〉. 〈hal-00712938v2〉
  • Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. Valérie Berthé and Christiane Frougny and Natacha Portier and Marie-Françoise Roy and Anne Siegel. École des Jeunes Chercheurs en Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30, 2012. 〈hal-00755333〉
  • Sylvie Boldo, Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-point Algorithms in Coq. Elisardo Antelo and David Hough and Paolo Ienne. Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Jul 2011, Tübingen, Germany. pp.243-252, 〈10.1109/ARITH.2011.40〉. 〈inria-00534854v2〉
  • Sylvie Boldo, Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. César Muñoz. Second NASA Formal Methods Symposium (NFM 2010), Apr 2010, Washington D.C., United States. NASA/CP-2010-216215, pp.14-23, 2010. 〈inria-00534410〉
  • Sylvie Boldo. Formal verification of numerical programs: from C annotated programs to Coq proofs. NSV-3: Third International Workshop on Numerical Software Verification, Jul 2010, Edinburgh, Scotland, United Kingdom. 2010. 〈inria-00534400〉
  • Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. Matt Kaufmann and Lawrence C. Paulson. ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, 6172, pp.147-162, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14052-5_12〉. 〈inria-00450789v3〉
  • Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. 5625, pp.59-74, 2009, 〈10.1007/978-3-642-02614-0_10〉. 〈inria-00432726〉
  • Sylvie Boldo, Marc Daumas, Pascal 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, 2008. 〈hal-00135090v3〉
  • Sylvie Boldo, César Muñoz. Provably Faithful Evaluation of Polynomials. 21st Annual ACM Symposium on Applied Computing, Apr 2006, Dijon, France, 2006. 〈inria-00000892〉
  • Sylvie Boldo, Guillaume Melquiond. When double rounding is odd. 17th IMACS World Congress, Jul 2005, Paris, France. pp.11, 2004. 〈inria-00070603v2〉
  • Sylvie Boldo, Jean-Michel Muller. Some Functions Computable with a Fused-mac. Paolo Montuschi, Eric Schwarz. 17th IEEE Symposium on Computer Arithmetic, Jun 2005, Cape Cod, Massachusetts, USA, pp.52-58, 2005. 〈inria-00000895〉
  • Ren Cang Li, Sylvie Boldo, Marc Daumas. Theorems on Efficient Argument Reductions. IEEE. 16th IEEE Symposium on Computer Arithmetic, 2003, Santiago de Compostela, Spain. IEEE, pp.129-136, 2003, 〈10.1109/ARITH.2003.1207670〉. 〈hal-00156244〉
  • Sylvie Boldo, Marc Daumas. Properties of the subtraction valid for any floating point system. 7th International Workshop on Formal Methods for Industrial Critical Systems, 2002, Málaga, Spain. pp.137-149, 0000. 〈inria-00072115〉

Poster1 document

  • Nguyen Thi Minh Tuyen, Sylvie Boldo, Claude Marché. Formal proofs of numerical programs. Forum Digitéo, Oct 2010, Palaiseau, France. 〈inria-00536135〉

Ouvrage (y compris édition critique et traduction)1 document

  • Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Sylvie Boldo, Denis Bouhineau, et al.. Une introduction à la science informatique pour les enseignants de la discipline en lycée. Gilles Dowek. CRDP Paris, pp.376, 2011, Repères pour agir (RPA disciplines & compétences), Christine Moulin, 978-2-86631-188-9. 〈hal-00765226〉

Chapitre d'ouvrage1 document

  • 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-01089095〉

Autre publication1 document

  • Thierry Vieville, Sylvie Boldo, Florent Masseglia, Pierre Bernhard. « Structures : organisation, complexité, dynamique » des mot-clés au sens inattendu. Article de vulgarisation sur pixees.fr. 2015. 〈hal-01238442〉

Pré-publication, Document de travail2 documents

  • Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound. 2013. 〈hal-00862653〉
  • Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Thery. Computer validated proofs of a toolset for adaptable arithmetic. 21 pages, web links. 2001. 〈hal-00018530〉

Rapport2 documents

  • Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, et al.. Médiation Scientifique : une facette de nos métiers de la recherche. [Interne] none. 2013, pp.34. 〈hal-00804915〉
  • Marc Daumas, Sylvie Boldo. Necessary and sufficient conditions for exact floating point operations. [Research Report] RR-4644, INRIA. 2002. 〈inria-00071941〉

HDR1 document

  • Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Computer Arithmetic. Université Paris-Sud, 2014. 〈tel-01089643〉