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] 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 ]
[2] 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 | .pdf ]
[1] Diane Gallois-Wong, Sylvie Boldo, and Pascal Cuoq. Optimal inverse projection of floating-point addition. Numerical Algorithms, 2019. [ bib | DOI | full text on HAL | .pdf ]

Conferences

[16] Jean-Christophe Filliâtre. Deductive verification of OCaml libraries. In 15th International Conference on integrated Formal Methods, Bergen, Norway, December 2019. Invited talk. [ bib | full text on HAL ]
[15] 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 ]
[14] Florian Steinberg, Holger Thies, and Laurent Théry. Quantitative continuity and Computable Analysis in Coq. In ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Portland, United States, September 2019. The version accepted to the conference can be accessed at https://drops.dagstuhl.de/opus/volltexte/2019/11083/. [ bib | DOI | full text on HAL ]
Keywords: Computable analysis ; Coq ; Contionuous functionals ; Discontinuity ; Closed choice on the natura
[13] 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, volume 12031 of Lecture Notes in Computer Science, New York, United States, July 2019. [ bib | DOI | full text on HAL ]
[12] Thibault Hilaire, Hacène Ouzia, and Benoit Lopez. Optimal Word-Length Allocation for the Fixed-Point Implementation of Linear Filters and Controllers. In ARITH 2019 - IEEE 26th Symposium on Computer Arithmetic, pages 175--182, Kyoto, Japan, June 2019. IEEE. [ bib | DOI | full text on HAL | .pdf ]
Keywords: fixed-point arithmetic ; word-length allocation
[11] Florian Faissole. Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matriciels. In AFADL 2019 - 18e journées Approches Formelles dans l'Assistance au Développement de Logiciels, Toulouse, France, June 2019. [ bib | full text on HAL ]
[10] 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 ]
[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] Cláudio Belo Lourenço, Maria João Frade, and Jorge Sousa Pinto. A Generalized Program Verification Workflow Based on Loop Elimination and SA Form. In FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering, Montreal, Canada, May 2019. [ bib | full text on HAL | .pdf ]
[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] 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 ]
[5] 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 ]
[4] 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 ]
[3] 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 | full text on HAL ]
[2] 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 ]
[1] Raphaël Rieu-Helft. Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP. 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 ]

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.

[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] 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 ]
[4] 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 ]
[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] 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 ]
[1] The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.9, 2019. http://coq.inria.fr. [ bib | http ]

Back

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


This page was generated by bibtex2html.