Wiki Agenda Contact Version française

Publications 2018

Back

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

Books and book chapters

Journals

[3] Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally verified approximations of definite integrals. Journal of Automated Reasoning, March 2018. [ bib | full text on HAL ]
[2] Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. Journal of Automated Reasoning, 60(3):365--383, 2018. [ bib | DOI | full text on HAL ]
[1] Sylvain Dailler, David Hauzar, Claude Marché, and Yannick Moy. Instrumenting a weakest precondition calculus for counterexample generation. Journal of Logical and Algebraic Methods in Programming, 99:97--113, 2018. [ bib | full text on HAL ]
Keywords: Deductive Program Verification ; Weakest Precondition Calculus ; Satisfiability Modulo Theories ; Counterexamples

Conferences

[7] Guillaume Melquiond and Raphaël Rieu-Helft. A Why3 framework for reflection proofs and its application to GMP's algorithms. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, 9th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, Oxford, United Kingdom, July 2018. [ bib | full text on HAL ]
[6] Sylvie Boldo, Florian Faissole, and Vincent Tourneur. A formally-proved algorithm to compute the correct average of decimal floating-point numbers. In 25th IEEE Symposium on Computer Arithmetic, Amherst, MA, United States, June 2018. [ bib | full text on HAL ]
[5] Pierre Roux, Mohamed Iguernlala, and Sylvain Conchon. A non-linear arithmetic procedure for control-command software verification. In 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Thessalonique, Greece, April 2018. [ bib | full text on HAL ]
[4] Florian Faissole and Bas Spitters. Preuves constructives de programmes probabilistes. In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL ]
[3] Florian Faissole. Définir le fini : deux formalisations d'espaces de dimension finie. In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL | .pdf ]
[2] Raphaël Rieu-Helft. Un mécanisme d'extraction vers C pour Why3. In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL | .pdf ]
[1] Jean-Christophe Filliâtre, Mário Pereira, and Simão Melo de Sousa. Vérification de programmes fortement impératifs avec Why3. In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL | .pdf ]

PhD theses

[1] Martin Clochard. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. Thèse de doctorat, Université Paris-Saclay, March 2018. [ bib | full text on HAL ]

Misc.

[2] Diane Gallois-Wong, Sylvie Boldo, and Thibault Hilaire. A Coq formalization of digital filters. working paper or preprint, March 2018. [ bib | full text on HAL ]
[1] Sylvie Boldo and Nicolas Magaud, editors. Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL ]

Reports


Back

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


This page was generated by bibtex2html.