Wiki Agenda Contact Version française

Publications 2017

Back

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

Books and book chapters

[1] Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press - Elsevier, December 2017. [ bib | full text on HAL ]

Journals

[2] 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 ]
[1] Ran Chen, Martin Clochard, and Claude Marché. A formally proved, complete algorithm for path resolution with symbolic links. Journal of Formalized Reasoning, 10(1):51--66, 2017. [ bib | DOI | full text on HAL | http ]

Conferences

[20] Clément Fumex, Claude Marché, and Yannick Moy. Automating the verification of floating-point programs. In Andrei Paskevich and Thomas Wies, editors, Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ]
[19] Nicolas Jeannerod, Claude Marché, and Ralf Treinen. A formally verified interpreter for a shell-like programming language. In Andrei Paskevich and Thomas Wies, editors, Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ]
[18] Jean-Christophe Filliâtre. Why3 --- where programs meet provers. In KeY Symposium 2017, Rastatt, Germany, October 2017. Invited talk. [ bib ]
[17] 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 ]
[16] Florian Faissole. Formalization and closedness of finite dimensional subspaces. In SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, September 2017. [ bib | http | .pdf ]
Keywords: filters ; finite dimensional subspaces ; formalization of mathematics ; functional analysis ; formal proof ; Coq
[15] 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 ]
[14] Ran Chen and Jean-Jacques Lévy. A semi-automatic proof of strong connectivity. In 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Heidelberg, Germany, July 2017. [ bib | full text on HAL ]
[13] Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond. How to get an efficient yet verified arbitrary-precision integer library. In 9th Working Conference on Verified Software: Theories, Tools, and Experiments, volume 10712 of Lecture Notes in Computer Science, pages 84--101, Heidelberg, Germany, July 2017. [ bib | DOI | full text on HAL | .pdf ]
Keywords: arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier
[12] 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 ]
[11] Jean-Christophe Filliâtre. Why3 tutorial. In VerifyThis 2017, Uppsala, Sweden, April 2017. Invited tutorial. [ bib ]
[10] Nicolas Jeannerod. Le coquillage dans le CoLiS-mateur: formalisation d'un langage de programmation de type Shell. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib ]
[9] 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 ]
[8] 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 Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[7] Martin Clochard. Preuves taillées en biseau. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[6] Mário Pereira. Défonctionnaliser pour prouver. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]
[5] 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, volume 10427 of Lecture Notes in Computer Science, pages 419--435, 2017. [ bib | DOI | full text on HAL ]
[4] Raphaël Rieu-Helft and Pascal Cuoq. Result graphs for an abstract interpretation-based static analyzer. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib ]
[3] Sylvain Conchon, David Declerck, and Fatiha Zaïdi. Compiling parameterized x86-tso concurrent programs to cubicle-w. In Zhenhua Duan and Luke Ong, editors, International Conference on Formal Engineering Methods, number 10610 in Lecture Notes in Computer Science, pages 88--104, 2017. [ bib ]
[2] Florian Faissole and Bas Spitters. Synthetic topology in HoTT for probabilistic programming. In The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Paris, France, January 2017. [ bib | full text on HAL ]
[1] Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, and Mattias Roux. FAR-Cubicle - A new reachability algorithm for Cubicle. In Daryl Stewart and Georg Weissenbacher, editors, Formal Methods in Computer Aided Design, pages 172--175, 2017. [ bib | DOI | full text on HAL ]

PhD theses

Misc.

[6] Andrei Paskevich and Thomas Wies, editors. Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference VSTTE, number 10712 in Lecture Notes in Computer Science, Heidelberg, Germany, December 2017. Springer. [ bib | full text on HAL ]
[5] 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 ]
[4] Alessandro Abate and Sylvie Boldo, editors. 10th International Workshop on Numerical Software Verification. Springer, July 2017. [ bib | full text on HAL ]
[3] Jean-Christophe Filliâtre. Vérification déductive de programmes. Séminaire Acquérir une culture commune dans le domaine de l'informatique, lycée Diderot, Paris, May 2017. Séminaire invité. [ bib ]
[2] Florian Faissole and Bas Spitters. Synthetic topology in homotopy type theory for probabilistic programming. PPS 2017 - Workshop on probabilistic programming semantics, January 2017. Poster. [ bib | full text on HAL ]
[1] Sylvie Boldo and Julien Signoles, editors. Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | full text on HAL ]

Reports

[3] Lucas Baudin. Deductive verification with the help of abstract interpretation. Technical report, Univ Paris-Sud, November 2017. [ bib | full text on HAL ]
[2] Ilham Dami and Claude Marché. The CoLiS language: syntax, semantics and associated tools. Technical Report 0491, Inria, October 2017. [ bib | full text on HAL ]
[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.