Toccata

Publications 2015

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

Books and book chapters

[1]

Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. In Bruno Woltzenlogel Paleo and David Delahaye, editors, All about Proofs, Proofs for All, volume 55 of Studies in Logic (Mathematical logic and foundations). College Publications, January 2015. [ bib | http | .pdf ]

Keywords: Coq proof assistant ; Calculus of Inductive Constructions

Journals

[6]	Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41--62, June 2015. [ bib \| DOI \| full text on HAL ]
[5]	Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 54(2):135--163, February 2015. [ bib \| full text on HAL ]
[4]	François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Let's verify this with Why3. International Journal on Software Tools for Technology Transfer (STTT), 17(6):709--727, 2015. See also http://toccata.gitlabpages.inria.fr/toccata/gallery/fm2012comp.en.html. [ bib \| DOI \| full text on HAL ]
[3]	Claude Marché and Johannes Kanig. Bridging the gap between testing and formal verification in Ada development. ERCIM News, 100:38--39, January 2015. [ bib \| full text on HAL ]
[2]	Pierre Roux. Formal proofs of rounding error bounds. Journal of Automated Reasoning, 2015. [ bib \| DOI \| full text on HAL ] Keywords: floating-point arithmetic ; rounding error ; numerical analysis ; proof assistant ; Coq ; matrices ; Cholesky decomposition
[1]	Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry. Formally verified certificate checkers for hardest-to-round computation. Journal of Automated Reasoning, 54(1):1--29, 2015. [ bib \| DOI \| full text on HAL ] Keywords: formal proofs ; certificate checkers ; Hensel's lemma ; modular arithmetic

Conferences

[8]	Sylvie Boldo. Formal Verification of Programs Computing the Floating-Point Average. In Michael Butler, Sylvain Conchon, and Fatiha Zaïdi, editors, 17th International Conference on Formal Engineering Methods, volume 9407 of Lecture Notes in Computer Science, pages 17--32, Paris, France, November 2015. Springer. [ bib \| full text on HAL \| .pdf ]
[7]	Umut A. Acar, Arthur Charguéraud, and Mike Rainey. A Work-Efficient Algorithm for Parallel Unordered Depth-First Search. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, Austin, Texas, United States, November 2015. [ bib \| DOI \| full text on HAL \| http ]
[6]	Arthur Charguéraud and François Pottier. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In 6th International Conference on Interactive Theorem Proving (ITP), Nanjing, China, August 2015. [ bib \| DOI \| full text on HAL \| http ]
[5]	Martin Clochard, Jean-Christophe Filliâtre, and Andrei Paskevich. How to avoid proving the absence of integer overflows. In Arie Gurfinkel and Sanjit A. Seshia, editors, 7th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), volume 9593 of Lecture Notes in Computer Science, pages 94--109, San Francisco, California, USA, July 2015. Springer. [ bib \| full text on HAL ] Keywords: Why3
[4]	Catherine Lelay. How to express convergence for analysis in Coq. In The 7th Coq Workshop, Sophia Antipolis, France, June 2015. [ bib \| full text on HAL ] Keywords: Coq proof assistant ; Analysis ; Limits ; Filters ; Type-Classes ; Canonical Structures
[3]	Sylvie Boldo. Stupid is as stupid does: Taking the square root of the square of a floating-point number. In Sergiy Bogomolov and Matthieu Martel, editors, Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification, volume 317 of Electronic Notes in Theoretical Computer Science, pages 50--55, Seattle, WA, USA, April 2015. [ bib \| DOI \| full text on HAL ]
[2]	Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. Polymorphic functions with set-theoretic types. part 2: Local type inference and type reconstruction. In Proceedings of the 42st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India, January 2015. ACM Press. [ bib \| full text on HAL ]
[1]	Martin Clochard and Léon Gondelman. Double WP: vers une preuve automatique d'un compilateur. In Vingt-sixièmes Journées Francophones des Langages Applicatifs, Val d'Ajol, France, January 2015. [ bib \| full text on HAL ]

PhD theses

[1]	Catherine Lelay. Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée. Thèse de doctorat, Université Paris-Sud, June 2015. [ bib \| full text on HAL ]

Misc.

[2]	Thierry Vieville, Sylvie Boldo, Florent Masseglia, and Pierre Bernhard. Structures : organisation, complexité, dynamique des mot-clés au sens inattendu, April 2015. Article de vulgarisation sur pixees.fr. [ bib \| full text on HAL ]
[1]	Jean-Christophe Filliâtre. Vérification déductive de programmes. Mathematic Park, Institut Henri Poincaré, March 2015. Séminaire invité. [ bib \| http ]

Reports

[3]	Claire Dross, Clément Fumex, Jens Gerlach, and Claude Marché. High-level functional properties of bit-level programs: Formal specifications and automated proofs. Research Report 8821, Inria, December 2015. [ bib \| full text on HAL ]
[2]	François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.86.1. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.86.1 edition, May 2015. http://why3.org/download/manual-0.86.1.pdf. [ bib \| .pdf ]
[1]	Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Fast parallel graph-search with splittable and catenable frontiers. Technical report, Inria, January 2015. [ bib \| full text on HAL ]

Back