Wiki Agenda Contact Version française

Publications 2019

Back

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

Books and book chapters

[1] Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, and Kim Nguyen. Numérique et Sciences Informatiques, 30 leçons avec exercices corrigés. Ellipses, August 2019. [ bib | http ]

Journals

[4] Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally verified approximations of definite integrals. Journal of Automated Reasoning, 62(2):281--300, February 2019. [ bib | DOI | full text on HAL ]
[3] Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. IEEE Transactions on Computers, 2019. [ bib | DOI | full text on HAL ]
[2] Diane Gallois-Wong, Sylvie Boldo, and Pascal Cuoq. Optimal inverse projection of floating-point addition. Numerical Algorithms, 2019. [ bib | DOI | full text on HAL ]
[1] Eike Neumann and Florian Steinberg. Parametrised second-order complexity theory with applications to the study of interval computation. Theoretical Computer Science, 2019. [ bib | DOI | full text on HAL ]

Conferences

[12] Jean-Christophe Filliâtre. Deductive verification of OCaml libraries. In 15th International Conference on integrated Formal Methods, Bergen, Norway, December 2019. Invited talk. [ bib ]
[11] Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, and Mário Pereira. GOSPEL --- providing OCaml with a formal specification language. In Annabelle McIver and Maurice ter Beek, editors, FM 2019 23rd International Symposium on Formal Methods, Porto, Portugal, October 2019. [ bib | full text on HAL ]
[10] Benedikt Becker and Claude Marché. Ghost code in action: Automated verification of a symbolic interpreter. In Supratik Chakraborty and Jorge A.Navas, editors, Verified Software: Tools, Techniques and Experiments, Lecture Notes in Computer Science, New York, United States, July 2019. [ bib | full text on HAL ]
[9] Jean-Christophe Filliâtre. The Why3 tool for deductive verification and verified OCaml libraries. In Frama-C & SPARK Day 2019, Paris, France, June 2019. Invited talk. [ bib ]
[8] Guillaume Melquiond and Raphaël Rieu-Helft. Formal verification of a state-of-the-art integer square root. In Symposium on Computer Arithmetic, pages 183--186, Kyoto, Japan, June 2019. [ bib | full text on HAL ]
[7] Akitoshi Kawamura, Florian Steinberg, and Holger Thies. Second-order linear-time computability with applications to computable analysis. In 15th Annual Conference Theory and Applications of Models of Computation, volume 11436 of Lecture Notes in Computer Science, pages 337--358, Tokyo, Japan, April 2019. Springer. [ bib | full text on HAL ]
[6] Raphaël Rieu-Helft. Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP. In 30èmes Journées Francophones des Langages Applicatifs, January 2019. [ bib | full text on HAL ]
[5] Diane Gallois-Wong. Formalisation en Coq d'algorithmes de filtres numériques. In 30èmes Journées Francophones des Langages Applicatifs, January 2019. [ bib | full text on HAL ]
[4] Jean-Christophe Filliâtre. Retour sur 25 ans de programmation avec OCaml. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. Séminaire invité. [ bib ]
[3] Valentin Blot, Amina Bousalem, Quentin Garchery, and Chantal Keller. SMTCoq: automatisation expressive et extensible dans Coq. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. [ bib | full text on HAL ]
[2] Guillaume Melquiond. Computer arithmetic and formal proofs. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. [ bib | full text on HAL ]
[1] Sylvain Conchon and Mattias Roux. Reasoning about universal cubes in MCMT. In Yamine Aït Ameur and Shengchao Qin, editors, International Conference on Formal Engineering Methods, volume 11852 of Lecture Notes in Computer Science, pages 270--285. Springer, 2019. [ bib | full text on HAL ]

PhD theses

[1] Guillaume Melquiond. Formal Verification for Numerical Computations, and the Other Way Around. Habilitation à diriger des recherches, Université Paris Sud, April 2019. [ bib | full text on HAL ]

Misc.

[4] Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Regis-Gianas, Sighireanu Mihaela, and Ralf Treinen. Analysing installation scenarios of Debian packages. working paper or preprint, November 2019. [ bib | full text on HAL ]
[3] Sylvie Boldo, Christoph Q. Lauter, and Jean-Michel Muller. Emulating round-to-nearest-ties-to-zero ”augmented” floating-point operations using round-to-nearest-ties-to-even arithmetic. working paper or preprint, October 2019. [ bib | full text on HAL ]
[2] Florian Steinberg, Laurent Thery, and Holger Thies. Quantitative continuity and computable analysis in Coq. working paper or preprint, April 2019. [ bib | full text on HAL | .pdf ]
[1] Florian Steinberg and Holger Thies. Some formal proofs of isomorphy and discontinuity. Third Workshop on Mathematical Logic and its Applications, March 2019. [ bib | full text on HAL ]

Reports

[5] Nicolas Jeannerod, Yann Régis-Gianas, Claude Marché, Mihaela Sighireanu, and Ralf Treinen. Specification of UNIX utilities. Technical report, HAL Archives Ouvertes, October 2019. [ bib | full text on HAL ]
[4] Benedikt Becker, Claude Marché, Nicolas Jeannerod, and Ralf Treinen. Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. Technical report, HAL Archives Ouvertes, October 2019. [ bib | full text on HAL ]
[3] Léo Andrès. Vérification par preuve formelle de propriétés fonctionnelles d'algorithme de classification. Rapport de stage de M1, Université Paris Sud, August 2019. [ bib | full text on HAL ]
[2] The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.9, 2019. http://coq.inria.fr. [ bib | http ]
[1] Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, and Gidon Ernst. Verifythis 2018: A program verification competition. Research report, Université Paris-Saclay, January 2019. [ bib | full text on HAL ]

Back

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


This page was generated by bibtex2html.