Sites Inria

Version française

TOCCATA Research team

TOCCATA team publications

2019

Journal articles

titre
Formally Verified Approximations of Definite Integrals
auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
article
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.281-300. <10.1007/s10817-018-9463-7>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630143/file/main.pdf BibTex

Conference papers

titre
Formal Verification of a State-of-the-Art Integer Square Root
auteur
Guillaume Melquiond, Raphaël Rieu-Helft
article
2019 IEEE 26th Symposium on Computer Arithmetic (ARITH), Jun 2019, Kyoto, Japan
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02092970/file/main.pdf BibTex
titre
Formalisation en Coq d'algorithmes de filtres numériques
auteur
Diane Gallois-Wong
article
Journées Francophones des Langages Applicatifs (JFLA) 2019, Jan 2019, Les Rousses, France. Journées Francophones des Langages Applicatifs 2019.
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01929531/file/JFLA19-coq-filtres-num.pdf BibTex
titre
Arithmétique des Ordinateurs et Preuves Formelles
auteur
Guillaume Melquiond
article
Nicolas Magaud. 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. 2019,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02013540/file/article.pdf BibTex
titre
Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP
auteur
Raphaël Rieu-Helft
article
30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Rousses, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01943010/file/main.pdf BibTex

Documents associated with scientific events

titre
Some formal proofs of isomorphy and discontinuity
auteur
Florian Steinberg, Holger Thies
article
MLA 2019 - Third Workshop on Mathematical Logic and its Applications, Mar 2019, Nancy, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02019174/file/mla.pdf BibTex

Reports

titre
VerifyThis 2018: A Program Verification Competition
auteur
Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, Gidon Ernst
article
[Research Report] Université Paris-Saclay. 2019
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01981937/file/sttt-summary.pdf BibTex

Notes de synthèse

titre
Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels (Documents de soutenance)
auteur
Martin Clochard
article
2019
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02047458/file/french.pdf BibTex

2018

Journal articles

titre
Instrumenting a Weakest Precondition Calculus for Counterexample Generation
auteur
Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy
article
Journal of Logical and Algebraic Methods in Programming, Elsevier, 2018, 99, pp.97-113
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01802488/file/jlamp.pdf BibTex
titre
The Matrix Reproved
auteur
Martin Clochard, Léon Gondelman, Mário Pereira
article
Journal of Automated Reasoning, Springer Verlag, 2018, 60 (3), pp.365-383. <10.1007/s10817-017-9436-2>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01617437/file/main.pdf BibTex
titre
Towards Hardware IIR Filters Computing Just Right: Direct Form I Case Study
auteur
Anastasia Volkova, Matei Istoan, Florent De Dinechin, Thibault Hilaire
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, In press, <10.1109/TC.2018.2879432>
Accès au texte intégral et bibtex
https://hal.sorbonne-universite.fr/hal-01561052/file/LTICJR.pdf BibTex

Conference papers

titre
A Coq formalization of digital filters
auteur
Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire
article
Florian Rabe; William M. Farmer; Grant O. Passmore; Abdou Youssef. CICM 2018 - 11th Conference on Intelligent Computer Mathematics, Aug 2018, Hagenberg, Austria. pp.87--103, Intelligent Computer Mathematics. . <10.1007/978-3-319-96812-4_8>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01728828/file/CICM18.pdf BibTex
titre
Parameterized Complexity for Uniform Operators on Multidimensional Analytic Functions and ODE Solving
auteur
Akitoshi Kawamura, Florian Steinberg, Holger Thies
article
Wollic 2018 - International Workshop on Logic, Language, Information, and Computation, Jul 2018, Bogota, Colombia. Springer, WoLLIC 2018: Logic, Language, Information, and Computation, 10944, pp.223-236, 2018, Lecture Notes in Computer Science. <10.1007/978-3-662-57669-4_13>
Accès au bibtex
BibTex
titre
A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms
auteur
Guillaume Melquiond, Raphaël Rieu-Helft
article
Didier Galmiche; Stephan Schulz; Roberto Sebastiani. 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, 2018, Lecture Notes in Computer Science. . <10.1007/978-3-319-94205-6_13>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01699754/file/main.pdf BibTex
titre
Alt-Ergo 2.2
auteur
Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, Alain Mebsout
article
SMT Workshop: International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom. 2018,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01960203/file/Alt-Ergo-2.2--SMT-Workshop-2018.pdf BibTex
titre
Type-two polynomial-time and restricted lookahead
auteur
Bruce Kapron, Florian Steinberg
article
LICS 2018 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. ACM Press, LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pp.579-588, <10.1145/3209108.3209124>
Accès au bibtex
BibTex
titre
A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers
auteur
Sylvie Boldo, Florian Faissole, Vincent Tourneur
article
25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01772272/file/article-HAL.pdf BibTex
titre
A Non-linear Arithmetic Procedure for Control-Command Software Verification
auteur
Pierre Roux, Mohamed Iguernelala, Sylvain Conchon
article
24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Apr 2018, Thessalonique, Greece. Springer, 10806, pp.132-151, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01737737/file/submission.pdf BibTex
titre
Parametrised second-order complexity theory with applications to the study of interval computation
auteur
Eike Neumann, Florian Steinberg
article
DICE 2018 - Developments in Implicit Computational Complexity, Apr 2018, Thesaloniki, Greece
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02019134/file/SN.pdf BibTex
titre
Un mécanisme d'extraction vers C pour Why3
auteur
Raphaël Rieu-Helft
article
29èmes Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01653153/file/main.pdf BibTex
titre
Preuves constructives de programmes probabilistes
auteur
Florian Faissole, Bas Spitters
article
JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. 2018, 29èmes Journées Francophones des Langages Applicatifs.
Accès au bibtex
BibTex
titre
Vérification de programmes OCaml fortement impératifs avec Why3
auteur
Jean-Christophe Filliâtre, Mário Pereira, Simão Melo de Sousa
article
JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. pp.1-14
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01649989/file/main.pdf BibTex
titre
Définir le fini : deux formalisations d'espaces de dimension finie
auteur
Florian Faissole
article
JLFA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-mer, France. pp.1-6, 2018, 29èmes Journées Francophones des Langages Applicatifs
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01654457/file/jfla.pdf BibTex
titre
Lightweight Interactive Proving inside an Automatic Program Verifier
auteur
Sylvain Dailler, Claude Marché, Yannick Moy
article
Masci, Paolo; Monahan, Rosemary; Prevosto, Virgile. 4th Workshop on Formal Integrated Development Environment, 2018, Oxford, United Kingdom. Open Publishing Association, 284, 2018, Electronic Proceedings in Theoretical Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01936302/file/article.pdf BibTex

Directions of work or proceedings

titre
Journées Francophones des Langages Applicatifs 2018
auteur
Sylvie Boldo, Nicolas Magaud
article
Sylvie Boldo; Nicolas Magaud. Journées Francophones des Langages Applicatifs 2018, Jan 2018, Banyuls-sur-Mer, France. publié par les auteurs, 2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01707376/file/jfla2018.pdf BibTex

Books

titre
Handbook of Floating-point Arithmetic (2nd edition)
auteur
Jean-Michel Muller, Nicolas Brunie, Florent De Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Serge Torres
article
Birkhäuser Basel, pp.1-627, 2018, 978-3319765259. <10.1007/978-3-319-76526-6>
Accès au bibtex
BibTex

Documents associated with scientific events

titre
Comparing integrability and measurability in different models of computation
auteur
Christine Gaßner, Arno Pauly, Florian Steinberg
article
CIE 2018 - 14th Conference on Computability in Europe, Jul 2018, Kiel, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02019195/file/Steinberg.pdf BibTex

Reports

titre
Deductive Verification via Ghost Debugging
auteur
Martin Clochard, Andrei Paskevich, Claude Marché
article
[Research Report] RR-9219, Inria Saclay Ile de France. 2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01907894/file/RR-9219.pdf BibTex
titre
Démonstration automatique en Coq
auteur
Quentin Garchery
article
[Travaux universitaires] Paris Diderot; Laboratoire de recherche en informatique (LRI) UMR CNRS 8623, Université Paris-Sud. 2018
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01874777/file/D%C3%A9monstration%20automatique%20en%20Coq.pdf BibTex

Theses

titre
Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels
auteur
Martin Clochard
article
Autre [cs.OH]. Université Paris-Saclay, 2018. Français.
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01787689/file/76309_CLOCHARD_2018_archivage.pdf BibTex

Preprints, Working Papers, ...

titre
Optimal Inverse Projection of Floating-Point Addition
auteur
Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01939097/file/main.pdf BibTex
titre
Verification of Programs with Pointers in SPARK
auteur
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01936105/file/report.pdf BibTex
titre
Arithmetic approaches for rigorous design of reliable Fixed-Point LTI filters
auteur
Anastasia Volkova, Thibault Hilaire, Christoph Lauter
article
2018
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01918650/file/ArithmeticApproachesForLTIdesign.pdf BibTex
titre
Deductive Verification with Ghost Monitors
auteur
Martin Clochard, Claude Marché, Andrei Paskevich
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01926659/file/article.pdf BibTex
titre
Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods
auteur
Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
article
2018
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01883843/file/article_hal_uo.pdf BibTex
titre
A Toolchain to Produce Correct-by-Construction OCaml Programs
auteur
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich, Mário Pereira, Simão Melo de Sousa
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01783851/file/main.pdf BibTex

2017

Journal articles

titre
A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links
auteur
Ran Chen, Martin Clochard, Claude Marché
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2017, 10 (1)
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01652148/file/jfr7213.pdf BibTex
titre
On the robustness of the 2Sum and Fast2Sum algorithms
auteur
Sylvie Boldo, Stef Graillat, Jean-Michel Muller
article
ACM Transactions on Mathematical Software, Association for Computing Machinery, 2017, 44 (1),
Accès au texte intégral et bibtex
https://hal-ens-lyon.archives-ouvertes.fr/ensl-01310023/file/FaithfulTwoSum-Final-Fev2017.pdf BibTex

Conference papers

titre
Compiling Parameterized X86-TSO Concurrent Programs to Cubicle- W
auteur
Sylvain Conchon, David Declerck, Fatiha Zaïdi
article
19th International Conference on Formal Methods and Software Engineering, Nov 2017, Xi'an, China. Springer, LNCS, 10610, pp.88-104, Lecture Notes in Computer Science. <10.1007/978-3-319-68690-5_6>
Accès au bibtex
BibTex
titre
FAR-Cubicle — A new reachability algorithm for Cubicle
auteur
Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux
article
2017 Formal Methods in Computer-Aided Design (FMCAD), Oct 2017, Vienna, France. IEEE, <10.23919/FMCAD.2017.8102256>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01927220/file/main.pdf BibTex
titre
Formal Verification of a Floating-Point Expansion Renormalization Algorithm
auteur
Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu
article
8th International Conference on Interactive Theorem Proving (ITP'2017), Sep 2017, Brasilia, Brazil. 10499, 2017, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01512417/file/itp17.pdf BibTex
titre
Formalization and closedness of finite dimensional subspaces
auteur
Florian Faissole
article
SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630411/file/synasc_hal.pdf BibTex
titre
A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT
auteur
Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex
article
Viktor Kuncak; Rupak Majumdar. 29th International Conference on Computer Aided Verification, Jul 2017, Heidelberg, Germany. Springer, 10427, pp.419-435, 2017, Lecture Notes in Computer Science. . <10.1007/978-3-319-63390-9_22>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01522770/file/main.pdf BibTex
titre
Round-off Error Analysis of Explicit One-Step Numerical Integration Methods
auteur
Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
article
24th IEEE Symposium on Computer Arithmetic, Jul 2017, London, United Kingdom. . <10.1109/ARITH.2017.22>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01581794/file/arith_hal.pdf BibTex
titre
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library
auteur
Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
article
Andrei Paskevich; Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. 10712, pp.84-101, 2017, Lecture Notes in Computer Science. . <10.1007/978-3-319-72308-2_6>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01519732/file/main.pdf BibTex
titre
A Semi-automatic Proof of Strong connectivity
auteur
Ran Chen, Jean-Jacques Lévy
article
9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2017, Heidelberg, Germany
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01632947/file/17scct.pdf BibTex
titre
Automating the Verification of Floating-Point Programs
auteur
Clément Fumex, Claude Marché, Yannick Moy
article
Andrei Paskevich and Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools and Experiments, Jul 2017, Heidelberg, Germany. Springer, 10712, 2017, Lecture Notes in Computer Science.
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01534533/file/article.pdf BibTex
titre
A Formally Verified Interpreter for a Shell-like Programming Language
auteur
Nicolas Jeannerod, Claude Marché, Ralf Treinen
article
VSTTE 2017 - 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. 10712, 2017, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01534747/file/jeannerod-marche-treinen-vstte17.pdf BibTex
titre
Preuve formelle du théorème de Lax–Milgram
auteur
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
article
16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France.
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01581807/file/article_afadl.pdf BibTex
titre
Temporary Read-Only Permissions for Separation Logic
auteur
Arthur Charguéraud, François Pottier
article
Proceedings of the 26th European Symposium on Programming (ESOP 2017), Apr 2017, Uppsala, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01408657/file/readonlysep.pdf BibTex
titre
Synthetic topology in HoTT for probabilistic programming
auteur
Florian Faissole, Bas Spitters
article
The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Jan 2017, Paris, France.
Accès au bibtex
BibTex
titre
A Coq formal proof of the Lax–Milgram theorem
auteur
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
article
6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. . <10.1145/3018610.3018625>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01391578/file/article.pdf BibTex
titre
Preuves taillées en biseau
auteur
Martin Clochard
article
vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), Jan 2017, Gourette, France. vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA),
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01404935/file/main.pdf BibTex
titre
Défonctionnaliser pour prouver
auteur
Mário Pereira
article
JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01378068/file/main.pdf BibTex
titre
Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe
auteur
Ran Chen, Jean-Jacques Lévy
article
JFLA 2017 - Vingt-huitièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France. Vingt-huitièmes Journées Francophones des Langages Applicatifs
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01422215/file/16jfla.pdf BibTex

Directions of work or proceedings

titre
Verified Software: Theories, Tools, and Experiments, Revised Selected Papers Presented at the 9th International Conference VSTTE
auteur
Andrei Paskevich, Thomas Wies
article
VSTTE 2017 - 9th International Conference Verified Software. Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. Lecture Notes in Computer Science (10712), 2017, <10.1007/978-3-319-72308-2>
Accès au bibtex
BibTex
titre
10th International Workshop on Numerical Software Verification
auteur
Alessandro Abate, Sylvie Boldo
article
10th International Workshop on Numerical Software Verification, France. Springer, 2017
Accès au bibtex
BibTex
titre
Vingt-huitièmes Journées Francophones des Langages Applicatifs
auteur
Sylvie Boldo, Julien Signoles
article
Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France. Published by the authors, 2017
Accès au bibtex
BibTex

Other publications

titre
The Coq Proof Assistant, version 8.7.1
auteur
The Coq Development Team
article
Official Release. 2017, pp.1-571. <10.5281/zenodo.1133970>
Accès au bibtex
BibTex
titre
VOCAL – A Verified OCAml Library
auteur
Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, François Pottier
article
ML Family Workshop 2017. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01561094/file/main.pdf BibTex

Books

titre
Computer Arithmetic and Formal Proofs
auteur
Sylvie Boldo, Guillaume Melquiond
article
ISTE Press - Elsevier, pp.326, 2017, 9781785481123
Accès au bibtex
BibTex

Poster communications

titre
Synthetic topology in homotopy type theory for probabilistic programming
auteur
Florian Faissole, Bas Spitters
article
PPS 2017 - Workshop on probabilistic programming semantics , Jan 2017, Paris, France. pp.3
Accès au bibtex
BibTex

Reports

titre
Le langage CoLiS : syntaxe, sémantique et outillage
auteur
Ilham Dami, Claude Marché
article
[Rapport Technique] RT-0491, Inria Saclay Ile de France. 2017, pp.1-22
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01614488/file/RT-0491.pdf BibTex
titre
Automated Verification of Floating-Point Computations in Ada Programs
auteur
Clément Fumex, Claude Marché, Yannick Moy
article
[Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01511183/file/RR-9060.pdf BibTex

2016

Journal articles

titre
Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages
auteur
Umut Acar, Arthur Charguéraud, Mike Rainey
article
Journal of Functional Programming, Cambridge University Press (CUP), 2016, 26, <10.1017/S0956796816000101>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01409069/file/granularity_jfp16.pdf BibTex
titre
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
auteur
Érik Martin-Dorel, Guillaume Melquiond
article
Journal of Automated Reasoning, Springer Verlag, 2016, 57 (3), pp.187-217. <10.1007/s10817-015-9350-4>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01086460/file/article.pdf BibTex
titre
Formalization of Real Analysis: A Survey of Proof Assistants and Libraries
auteur
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2016, 26 (7), pp.1196-1233. <10.1017/S0960129514000437>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00806920/file/article.pdf BibTex
titre
The Spirit of Ghost Code
auteur
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
article
Formal Methods in System Design, Springer Verlag, 2016, 48 (3), pp.152-174. <10.1007/s10703-016-0243-x>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01396864/file/main.pdf BibTex
titre
Adding Decision Procedures to SMT Solvers using Axioms with Triggers
auteur
Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich
article
Journal of Automated Reasoning, Springer Verlag, 2016, 56 (4), pp.387-457. <10.1007/s10817-015-9352-2>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01221066/file/main.pdf BibTex

Conference papers

titre
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014
auteur
Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles
article
7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. Springer, 9952, pp.461--478, 2016, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01344110/file/paper063.pdf BibTex
titre
Dag-calculus: a calculus for parallel computation
auteur
Umut Acar, Arthur Charguéraud, Mike Rainey, Filip Sieczkowski
article
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), Sep 2016, Nara, Japan. pp.18 - 32, 2016, <10.1145/2951913.2951946>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01409022/file/dag_calculus_icfp16.pdf BibTex
titre
Formally Verified Approximations of Definite Integrals
auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
article
Jasmin Christian Blanchette; Stephan Merz. Interactive Theorem Proving, Aug 2016, Nancy, France. 9807, 2016, Lecture Notes in Computer Science. . <10.1007/978-3-319-43144-4_17>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01289616/file/main.pdf BibTex
titre
Iterators: where folds fail
auteur
Sylvie Boldo
article
Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01377155/file/abstract.pdf BibTex
titre
The Matrix Reproved (Verification Pearl)
auteur
Martin Clochard, Léon Gondelman, Mário Pereira
article
VSTTE 2016, Jul 2016, Toronto, Canada
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01316902/file/paper_12.pdf BibTex
titre
Producing All Ideals of a Forest, Formally (Verification Pearl)
auteur
Jean-Christophe Filliâtre, Mário Pereira
article
VSTTE 2016, Jul 2016, Toronto, Canada. pp.46 - 55, 2016, <10.1007/978-3-319-48869-1_4>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01316859/file/paper_6.pdf BibTex
titre
Computing a correct and tight rounding error bound using rounding-to-nearest
auteur
Sylvie Boldo
article
9th International Workshop on Numerical Software Verification, Jul 2016, Toronto, Canada. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01377152/file/article.pdf BibTex
titre
Counterexamples from Proof Failures in SPARK
auteur
David Hauzar, Claude Marché, Yannick Moy
article
Software Engineering and Formal Methods, Jul 2016, Vienna, Austria. Springer, 2016, Software Engineering and Formal Methods
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01314885/file/article.pdf BibTex
titre
A Modular Way to Reason About Iteration
auteur
Jean-Christophe Filliâtre, Mário Pereira
article
8th NASA Formal Methods Symposium, Jun 2016, Minneapolis, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01281759/file/main.pdf BibTex
titre
Specification and Proof of High-Level Functional Properties of Bit-Level Programs
auteur
Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché
article
NASA Formal methods, Jun 2016, Minneapolis, United States. Springer, 2016, NASA Formal methods
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01314876/file/article-final.pdf BibTex
titre
Itérer avec confiance
auteur
Jean-Christophe Filliâtre, Mário Pereira
article
Journées Francophones des Langages Applicatifs, Jan 2016, Saint-Malo, France.
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01240891/file/main.pdf BibTex
titre
Higher-order representation predicates in separation logic
auteur
Arthur Charguéraud
article
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), Jan 2016, St. Petersburg, FL, United States. ACM, pp.3 - 14, 2016, <10.1145/2854065.2854068>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01408670/file/horepr.pdf BibTex

Documents associated with scientific events

titre
Strongly Connected Components in graphs, formal proof of Tarjan1972 algorithm
auteur
Jean-Jacques Levy, Ran Chen
article
Groupe de travail LTP du GDR GPL , Nov 2016, Orsay, France. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01422227/file/scct72.pdf BibTex

Reports

titre
A Formal Proof of a Unix Path Resolution Algorithm
auteur
Ran Chen, Martin Clochard, Claude Marché
article
[Research Report] RR-8987, Inria. 2016, pp.27
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01406848/file/RR-8987.pdf BibTex
titre
Counterexamples from proof failures in the SPARK program verifier
auteur
David Hauzar, Claude Marché, Yannick Moy
article
[Research Report] RR-8854, Inria. 2016, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01271174/file/RR-8854.pdf BibTex

Theses

titre
Un système de types pragmatique pour la vérification déductive des programmes
auteur
Léon Gondelman
article
Logique en informatique [cs.LO]. Université Paris-Saclay, 2016. Français.
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01533090/file/73319_GONDELMAN_2016-diffusion.pdf BibTex

Preprints, Working Papers, ...

titre
Formal proofs of two algorithms for strongly connected components in graphs
auteur
Ran Chen, Jean-Jacques Levy
article
2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01422216/file/16sccs.pdf BibTex
titre
A Pragmatic Type System for Deductive Verification
auteur
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
article
2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01256434/file/main%20%281%29.pdf BibTex

2015

Journal articles

titre
Coquelicot: A User-Friendly Library of Real Analysis for Coq
auteur
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
article
Mathematics in Computer Science, Springer, 2015, 9 (1), pp.41-62. <10.1007/s11786-014-0181-1>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00860648/file/article.pdf BibTex
titre
Verified Compilation of Floating-Point Computations
auteur
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
article
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. <10.1007/s10817-014-9317-x>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00862689/file/floating-point-compcert.pdf BibTex
titre
Bridging the Gap between Testing and Formal Verification in Ada Development
auteur
Claude Marché, Johannes Kanig
article
ERCIM News, ERCIM, 2015, 100, pp.2.
Accès au bibtex
BibTex
titre
Formal Proofs of Rounding Error Bounds
auteur
Pierre Roux
article
Journal of Automated Reasoning, Springer Verlag, 2015, pp.23. . <10.1007/s10817-015-9339-z>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01091189/file/submission.pdf BibTex
titre
Formally verified certificate checkers for hardest-to-round computation
auteur
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, Laurent Théry
article
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (1), pp.1-29. <10.1007/s10817-014-9312-2>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00919498/file/Hensel-JAR.pdf BibTex
titre
Let's Verify This with Why3
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
article
Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727. <10.1007/s10009-014-0314-5>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00967132/file/main.pdf BibTex

Conference papers

titre
A Work-Efficient Algorithm for Parallel Unordered Depth-First Search
auteur
Umut A. Acar, Arthur Charguéraud, Mike Rainey
article
Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, Nov 2015, Austin, Texas, United States. <10.1145/2807591.2807651>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01245837/file/pdfs_sc15.pdf BibTex
titre
Formal Verification of Programs Computing the Floating-Point Average
auteur
Sylvie Boldo
article
Michael Butler; Sylvain Conchon; Fatiha Zaïdi. 17th International Conference on Formal Engineering Methods, Nov 2015, Paris, France. Springer, 9407, pp.17-32, 2015,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01174892/file/article.pdf BibTex
titre
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
auteur
Arthur Charguéraud, François Pottier
article
6th International Conference on Interactive Theorem Proving (ITP), Aug 2015, Nanjing, China. 2015, <10.1007/978-3-319-22102-1_9>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01245872/file/credits_itp15.pdf BibTex
titre
How to avoid proving the absence of integer overflows
auteur
Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich
article
Arie Gurfinkel and Sanjit A. Seshia. 7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States. Lecture Notes in Computer Science.
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01162661/file/main.pdf BibTex
titre
How to express convergence for analysis in Coq
auteur
Catherine Lelay
article
The 7th Coq Workshop, Jun 2015, Sophia Antipolis, France
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01169321/file/article.pdf BibTex
titre
Certificates for Parameterized Model Checking
auteur
Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi
article
FM 2015 - 20th International Symposium on Formal Methods, May 2015, Oslo, Norway. Springer, LNCS, 9109, pp.126-142, FM 2015: Formal Methods. <10.1007/978-3-319-19249-9_9>
Accès au bibtex
BibTex
titre
Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number
auteur
Sylvie Boldo
article
Sergiy Bogomolov and Matthieu Martel. Seventh and Eighth International Workshop on Numerical Software Verification, Apr 2015, Seattle, WA, United States. Electronic Notes in Theoretical Computer Science, pp.50--55, 2015,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01148409/file/article.pdf BibTex
titre
Double WP : Vers une preuve automatique d'un compilateur
auteur
Martin Clochard, Léon Gondelman
article
Journées Francophones des Langages Applicatifs, Jan 2015, Val d'Ajol, France. 2015,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094488/file/main.pdf BibTex
titre
Improving Type Error Messages in OCaml
auteur
Arthur Charguéraud
article
ML Family/OCaml Users and Developers workshops, 2015, Vancouver, Canada. Proceedings ML Family/OCaml Users and Developers workshops, 198, pp.80-97, 2015, Electronic Proceedings in Theoretical Computer Science. <10.4204/EPTCS.198.4>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01245843/file/ocaml_errors.pdf BibTex

Book sections

titre
Introduction to the Calculus of Inductive Constructions
auteur
Christine Paulin-Mohring
article
Bruno Woltzenlogel Paleo; David Delahaye. All about Proofs, Proofs for All, 55, College Publications, 2015, Studies in Logic (Mathematical logic and foundations), 978-1-84890-166-7.
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094195/file/CIC.pdf BibTex

Other publications

titre
« Structures : organisation, complexité, dynamique » des mot-clés au sens inattendu
auteur
Thierry Vieville, Sylvie Boldo, Florent Masseglia, Pierre Bernhard
article
Article de vulgarisation sur pixees.fr. 2015
Accès au bibtex
BibTex

Reports

titre
High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs
auteur
Claire Dross, Clément Fumex, Jens Gerlach, Claude Marché
article
[Research Report] RR-8821, Inria Saclay. 2015, pp.52
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01238376/file/RR-8821.pdf BibTex
titre
Fast Parallel Graph-Search with Splittable and Catenable Frontiers
auteur
Umut A. Acar, Arthur Charguéraud, Mike Rainey
article
[Technical Report] Inria. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01089125/file/psearch.pdf BibTex

2014

Journal articles

titre
Innocuous Double Rounding of Basic Arithmetic Operations
auteur
Pierre Roux
article
Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, 7 (1), pp.131-142. . <10.6092/issn.1972-5787/4359>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01091186/file/submission.pdf BibTex
titre
Des ordinateurs capables de calculer plus juste
auteur
Jean-Michel Muller, Sylvie Boldo
article
La Recherche : l'actualité des sciences, société d'éditions scientifiques, 2014, pp.46-53
Accès au bibtex
BibTex
titre
Trusting computations: a mechanized proof from partial differential equations to actual program
auteur
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
article
Computers and Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. <10.1016/j.camwa.2014.06.004 >
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00769201/file/RR-8197.pdf BibTex
titre
Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study
auteur
Claude Marché
article
Science of Computer Programming, Elsevier, 2014, 93 (3), pp.279-296. &#x27E8;10.1016/j.scico.2014.04.003&#x27E9;
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00967124/file/main.pdf BibTex

Conference papers

titre
Formal verification of tricky numerical computations
auteur
Sylvie Boldo
article
Marco Nehmeier. 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Sep 2014, Würzburg, Germany. pp.39, 2014,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01088692/file/article.pdf BibTex
titre
Theory and Practice of Chunked Sequences
auteur
Umut A. Acar, Arthur Charguéraud, Mike Rainey
article
Schulz, Andreas S. and Wagner, Dorothea. European Symposium on Algorithms, Sep 2014, Wrocław, Poland. Springer Berlin Heidelberg, Algorithms - ESA 2014, 8737, pp.25 - 36, 2014, Lecture Notes in Computer Science. <10.1007/978-3-662-44777-2_3>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087245/file/chunkedseq.pdf BibTex
titre
The Spirit of Ghost Code
auteur
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
article
CAV 2014, Computer Aided Verification - 26th International Conference, Jul 2014, Vienna Summer Logic 2014, Austria. Computer Aided Verification - 26th International Conference, 2014, Held as Part of the Vienna Summer of Logic, 2014, Vienna, Austria, July 18-22, 2014. Proceedings,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00873187/file/main.pdf BibTex
titre
Automating the verification of floating-point algorithms
auteur
Guillaume Melquiond
article
12th International Workshop on Satisfiability Modulo Theories, Jul 2014, Wien, Austria
Accès au bibtex
BibTex
titre
Automatically verified implementation of data structures based on AVL trees
auteur
Martin Clochard
article
Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01067217/file/main.pdf BibTex
titre
Formalizing Semantics with an Automatic Program Verifier
auteur
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
article
Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01067197/file/main.pdf BibTex
titre
Tuning the Alt-Ergo SMT Solver for B Proof Obligations
auteur
Sylvain Conchon, Mohamed Iguernelala
article
ABZ, Jun 2014, Toulouse, France. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093000/file/alt-ergo.pdf BibTex
titre
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations
auteur
David Delahaye, Catherine Dubois, Claude Marché, David Mentré
article
Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. Springer, 8477, pp.290-293, 2014, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00998092/file/bware_ABZ_14_.pdf BibTex
titre
Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B
auteur
David Delahaye, Claude Marché, David Mentré
article
Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2014, Paris, France. EasyChair, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00998094/file/afadl2014_submission_6.pdf BibTex
titre
A Coq Formalization of the Relational Data Model
auteur
Véronique Benzaken, Évelyne Contejean, Stefania Dumbrava
article
Zhong Shao. ESOP - 23rd European Symposium on Programming, Apr 2014, Grenoble, France. Springer, 2014, Lecture Notes in Computer Science
Accès au bibtex
BibTex
titre
A Trusted Mechanised JavaScript Specification
auteur
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith
article
POPL 2014 - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00910135/file/jscert_popl.pdf BibTex
titre
Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières
auteur
Sylvain Conchon, Luc Maranget, Alain Mebsout, David Declerck
article
JFLA, Jan 2014, Fréjus, France. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01088655/file/main.pdf BibTex
titre
Verified Programs with Binders
auteur
Martin Clochard, Claude Marché, Andrei Paskevich
article
Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ACM Press, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00913431/file/plpv03-clochard.pdf BibTex
titre
Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search
auteur
Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama
article
POPL - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. ACM Press, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00920955/file/clochard14popl.pdf BibTex

Book sections

titre
Même les ordinateurs font des erreurs !
auteur
Sylvie Boldo
article
Martin Andler; Liliane Bel; Sylvie Benzoni-Gavage; Thierry Goudon; Cyril Imbert; Antoine Rousseau. Brèves de maths, Nouveau Monde Editions, pp.136-137, 2014, 978-2-36583-896-2
Accès au bibtex
BibTex

Habilitation à diriger des recherches

titre
Deductive Formal Verification: How To Make Your Floating-Point Programs Behave
auteur
Sylvie Boldo
article
Computer Arithmetic. Université Paris-Sud, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01089643/file/hdr.pdf BibTex
titre
Facettes de la preuve
auteur
Évelyne Contejean
article
Logique en informatique [cs.LO]. Université Paris-Sud, 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01089490/file/main.pdf BibTex

Books

titre
Apprendre à programmer avec OCaml
auteur
Sylvain Conchon, Jean-Christophe Filliâtre
article
Eyrolles, pp.429, 2014, Noire, 9782212136784
Accès au bibtex
BibTex

2013

Journal articles

titre
Some issues related to double roundings
auteur
Érik Martin-Dorel, Guillaume Melquiond, Jean-Michel Muller
article
BIT Numerical Mathematics, Springer Verlag, 2013, 53 (4), pp.897-924. <10.1007/s10543-013-0436-2>
Accès au texte intégral et bibtex
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00644408/file/Version_Finale_DoubleRoundings.pdf BibTex
titre
Wave equation numerical resolution: a comprehensive mechanized proof of a C program
auteur
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
article
Journal of Automated Reasoning, Springer Verlag, 2013, 50 (4), pp.423-456. <10.1007/s10817-012-9255-4>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00649240/file/RR-7826.pdf BibTex
titre
Numerical Approximation of the Masser-Gramain Constant to Four Decimal Digits: delta=1.819...
auteur
Guillaume Melquiond, W. Georg Nowak, Paul Zimmermann
article
Mathematics of Computation, American Mathematical Society, 2013, 82, pp.1235-1246. <10.1090/S0025-5718-2012-02635-4>
Accès au bibtex
BibTex

Conference papers

titre
Invariants for Finite Instances and Beyond
auteur
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, Fatiha Zaïdi
article
Formal Methods in Computer-Aided Design (FMCAD), Oct 2013, Portland, Oregon, United States. pp.61-68, 2013, <10.1109/FMCAD.2013.6679392>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00924640/file/conchon-fmcad2013.pdf BibTex
titre
Automations for verifying floating-point algorithms
auteur
Guillaume Melquiond
article
5th Coq Workshop, Jul 2013, Rennes, France
Accès au bibtex
BibTex
titre
A New Formalization of Power Series in Coq
auteur
Catherine Lelay
article
The 5th Coq Workshop, Jul 2013, Rennes, France. 2013,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00880212/file/article.pdf BibTex
titre
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus
auteur
Daisuke Ishii, Guillaume Melquiond, Shin Nakajima
article
Einar Broch Johnsen and Luigia Petre. iFM - 10th International Conference on Integrated Formal Methods - 2013, Jun 2013, Turku, Finland. Springer, 7940, pp.139-153, 2013, <10.1007/978-3-642-38613-8_10>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00806701/file/article.pdf BibTex
titre
One Logic To Use Them All
auteur
Jean-Christophe Filliâtre
article
Maria Paola Bonacina. CADE 24 - the 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, NY, United States. Springer, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00809651/file/main.pdf BibTex
titre
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
auteur
Jasmin Blanchette, Andrei Paskevich
article
M.P. Bonacina. CADE - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.414-420, 2013, LNCS
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00825086/file/tff1short.pdf BibTex
titre
Preserving User Proofs Across Specification Changes
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
article
Ernie Cohen and Andrey Rybalchenko. Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. Springer, 8164, pp.191-201, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00875395/file/main.pdf BibTex
titre
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
auteur
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
article
Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. IEEE, pp.107-115, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00743090/file/article.pdf BibTex
titre
How to Compute the Area of a Triangle: a Formal Revisit
auteur
Sylvie Boldo
article
Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang. 21st IEEE International Symposium on Computer Arithmetic, Apr 2013, Austin, TX, United States. IEEE, pp.91-98, 2013, <10.1109/ARITH.2013.29>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00790071/file/article.pdf BibTex
titre
Why3 -- Where Programs Meet Provers
auteur
Jean-Christophe Filliâtre, Andrei Paskevich
article
ESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy. Springer, 7792, 2013, LNCS
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00789533/file/main.pdf BibTex
titre
Pretty-Big-Step Semantics
auteur
Arthur Charguéraud
article
Matthias Felleisen and Philippa Gardner. 22nd European Symposium on Programming (ESOP), Mar 2013, Rome, Italy. Springer, 2013, Proceedings of the 22nd European Symposium on Programming
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00798227/file/prettybigstep.pdf BibTex
titre
Scheduling Parallel Programs by Work Stealing with Private Deques
auteur
Umut Acar, Arthur Charguéraud, Mike Rainey
article
PPOPP - 18th ACM SIGPLAN symposium on Principles and practice of parallel programming, Feb 2013, Shenzhen, China. ACM New York, NY, USA, pp.219-228, 2013, Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863028/file/full.pdf BibTex
titre
combine : une bibliothèque OCaml pour la combinatoire
auteur
Rémy El Sibaïe, Jean-Christophe Filliâtre
article
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00779431/file/jfla2013-05.pdf BibTex
titre
Calcul de plus faible précondition, revisité en Why3
auteur
Claude Marché, Asma Tafat
article
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs - 2013, Feb 2013, Aussois, France. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00778791/file/jfla2013-01.pdf BibTex
titre
Vérification de systèmes paramétrés avec Cubicle
auteur
Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi
article
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs - 2013, Feb 2013, Aussois, France. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00778832/file/jfla2013-02.pdf BibTex
titre
Deductive Program Verification
auteur
Jean-Christophe Filliâtre
article
Nate Foster and Philippa Gardner and Alan Schmitt and Gareth Smith and Peter Thieman and Tobias Wrigstad. Programming Languages Mentoring Workshop (PLMW 2013), Jan 2013, Rome, Italy. 2013
Accès au bibtex
BibTex

Book sections

titre
Arithmétique des ordinateurs et preuves formelles
auteur
Sylvie Boldo, Guillaume Melquiond
article
Informatique mathématique : Une photographie en 2013, 2013
Accès au bibtex
BibTex

Directions of work or proceedings

titre
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings
auteur
Sandrine Blazy, Christine Paulin-Mohring, David Pichardie
article
Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Rennes, France. 7998, Springer, pp.500, 2013, Lecture Notes in Computer Science, <10.1007/978-3-642-39634-2>
Accès au bibtex
BibTex

Other publications

titre
The Why3 platform 0.81
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
article
Tutorial and Reference Manual. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00822856/file/manual-0.81.pdf BibTex

Books

titre
Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python
auteur
Judicaël Courant, Marc De Falco, Stéphane Gonnord, Jean-Christophe Filliâtre, Sylvain Conchon, Gilles Dowek, Benjamin Wack
article
Eyrolles, pp.1-390, 2013, 978-2-212-13700-2
Accès au bibtex
BibTex

Reports

titre
Atomic Read-Modify-Write Operations are Unnecessary for Shared-Memory Work Stealing
auteur
Umut Acar, Arthur Charguéraud, Stefan Muller, Mike Rainey
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00910130/file/main.pdf BibTex
titre
Médiation Scientifique : une facette de nos métiers de la recherche
auteur
Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie De Quatrebarbes, Stéphane Laurent
article
[Interne] none. 2013, pp.34
Accès au bibtex
BibTex

Theses

titre
Preuves par raffinement de programmes avec pointeurs
auteur
Asma Tafat
article
Autre [cs.OH]. Université Paris Sud - Paris XI, 2013. Français.
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00874679/file/VD2_tafatbouzid_asma_06062013.pdf BibTex
titre
Strengthening the heart of an SMT-solver : Design and implementation of efficient decision procedures
auteur
Mohamed Iguernelala
article
Other [cs.OH]. Université Paris Sud - Paris XI, 2013. English.
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00842555/file/VD2_IGUERNELALA_MOHAMED_10062013.pdf BibTex
titre
Certification of a Tool Chain for Deductive Program Verification
auteur
Paolo Herms
article
Other [cs.OH]. Université Paris Sud - Paris XI, 2013. English.
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00789543/file/VD2_HERMS_PAOLO_14012013.pdf BibTex

Preprints, Working Papers, ...

titre
How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound
auteur
Sylvie Boldo
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00862653/file/article.pdf BibTex
titre
Adding Decision Procedures to SMT Solvers using Axioms with Triggers
auteur
Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00915931/file/dross-article.pdf BibTex
titre
A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo
auteur
Sylvain Conchon, Mohamed Iguernelala, Alain Mebsout
article
2013
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00924646/file/conchon-synasc2013.pdf BibTex

2012

Journal articles

titre
Floating-point arithmetic in the Coq system
auteur
Guillaume Melquiond
article
Information and Computation, Elsevier, 2012, 216, pp.14-23. <10.1016/j.ic.2011.09.005>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00797913/file/article.pdf BibTex

Conference papers

titre
Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives
auteur
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
article
Chris Hawblitzel and Dale Miller. CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. Springer, 7679, pp.289-304, 2012, Lecture Notes in Computer Science. <10.1007/978-3-642-35308-6_22>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00712938/file/article.pdf BibTex
titre
Separation Predicates: a Taste of Separation Logic in First-Order Logic
auteur
François Bobot, Jean-Christophe Filliâtre
article
14th International Conference on Formal Ingineering Methods (ICFEM), Nov 2012, Kyoto, Japan. Springer, 7635, pp.167-181, 2012, Lecture Notes in Computer Science. <10.1007/978-3-642-34281-3_14>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00825088/file/bobot12icfem.pdf BibTex
titre
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
auteur
Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala
article
Pascal Fontaine; Amit Goel. 10th International Workshop on Satisfiability Modulo Theories, Jun 2012, Manchester, United Kingdom. pp.12-21, 2012,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01785166/file/article.pdf BibTex
titre
The 2nd Verified Software Competition: Experience Report
auteur
Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump
article
Vladimir Klebanov, Bernhard Beckert, Armin Biere, Geoff Sutcliffe. COMPARE 2012, Comparative Empirical Evaluation of Reasoning Systems, 1st Intl. Workshop, Jun 2012, Manchester, United Kingdom. CEUR Workshop Proceedings, 873, pp.36-49, 2012, CEUR Workshop Proceedings.
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00798777/file/main.pdf BibTex
titre
Arithmétique des ordinateurs et preuves formelles
auteur
Sylvie Boldo, Guillaume Melquiond
article
Valérie Berthé and Christiane Frougny and Natacha Portier and Marie-Françoise Roy and Anne Siegel. École des Jeunes Chercheurs en Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00755333/file/main.pdf BibTex

2011

Journal articles

titre
Real-Time Monitoring of Ocaml programs
auteur
Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, Guillaume Von Tokarski
article
Stud. Inform. Univ., 2011, 9 (1), pp.159-185
Accès au bibtex
BibTex

Conference papers

titre
The COST IC0701 Verification Competition 2011
auteur
Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, Radu Grigore, Marieke Huisman, Vladimir Klebanov, Claude Marché, Rosemary Monahan, Wojciech Mostowski, Nadia Polikarpova, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, Mattias Ulbrich
article
Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, 2011, Torino, Italy. Springer, 7421, 2012, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00789525/file/costcomp2011.pdf BibTex

2010

Journal articles

titre
Un algorithme de découpe de gâteau
auteur
Sylvie Boldo
article
Interstices, INRIA, 2010,
Accès au bibtex
BibTex

2009

Journal articles

titre
Demandez le programme
auteur
Sylvie Boldo
article
Interstices, INRIA, 2009,
Accès au bibtex
BibTex

2008

Journal articles

titre
Idée reçue : L’informatique, ce n’est pas pour les filles
auteur
Sylvie Boldo, Thierry Vieville
article
Interstices, INRIA, 2008,
Accès au bibtex
BibTex
titre
Pourquoi mon ordinateur calcule-t-il faux ?
auteur
Sylvie Boldo, Joanna Jongwane
article
Interstices, INRIA, 2008,
Accès au bibtex
BibTex

2005

Conference papers

titre
Reflecting Proofs in First-Order Logic with Equality
auteur
Évelyne Contejean, Pierre Corbineau
article
Robert Nieuwenhuis. 20th International Conference on Automated Deduction (CADE-20), 2005, Tallinn, Estonia. Springer, 3632, pp.7--22, 2005, LNAI. <10.1007/11532231_2>
Accès au bibtex
BibTex