Wiki Agenda Contact Version française

Publications 2017

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports

Books and book chapters

Journals

[1] Sylvie Boldo, Stef Graillat, and Jean-Michel Muller. On the robustness of the 2Sum and Fast2Sum algorithms. ACM Transactions on Mathematical Software, 44(1), July 2017. [ bib | full text on HAL | .pdf ]

Conferences

[11] Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, and Valentina Popescu. Formal Verification of a Floating-Point Expansion Renormalization Algorithm. In Proceedings of the 8th International Conference on Interactive Theorem Proving, Brasilia, Brazil, September 2017. [ bib | full text on HAL | .pdf ]
[10] Clément Fumex, Claude Marché, and Yannick Moy. Automating the verification of floating-point programs. In Andrei Paskevich and Thomas Wies, editors, 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Heidelberg, Germany, July 2017. Springer. [ bib | full text on HAL ]
[9] Nicolas Jeannerod, Claude Marché, and Ralf Treinen. A formally verified interpreter for a shell-like programming language. In Andrei Paskevich and Thomas Wies, editors, 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Heidelberg, Germany, July 2017. Springer. [ bib | full text on HAL ]
[8] Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. In 24th IEEE Symposium on Computer Arithmetic, London, United Kingdom, July 2017. [ bib | DOI | full text on HAL | .pdf ]
[7] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. Preuve formelle du théorème de Lax--Milgram. In 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Montpellier, France, June 2017. [ bib | full text on HAL | .pdf ]
[6] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq Formal Proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79--89, New York, NY, USA, January 2017. ACM. [ bib | DOI | full text on HAL | .pdf ]
[5] Ran Chen and Jean-Jacques Lévy. Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[4] Martin Clochard. Preuves taillées en biseau. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[3] Mário Pereira. Défonctionnaliser pour prouver. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[2] Sylvain Conchon, Mohamed Iguernlala, Kailiang Ji, Guillaume Melquiond, and Clément Fumex. A three-tier strategy for reasoning about floating-point numbers in SMT. In Computer Aided Verification, 2017. [ bib | full text on HAL ]
[1] Raphaël Rieu-Helft and Pascal Cuoq. Result graphs for an abstract interpretation-based static analyzer. In Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib ]

PhD theses

Misc.

[1] Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and François Pottier. VOCAL -- A Verified OCaml Library. ML Family Workshop, September 2017. [ bib | full text on HAL ]

Reports

[1] Clément Fumex, Claude Marché, and Yannick Moy. Automated verification of floating-point computations in Ada programs. Research Report RR-9060, Inria, April 2017. [ bib | full text on HAL ]

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports


This page was generated by bibtex2html.