Publications HAL de la structure toccata

2021

Journal articles

ref_biblio
Jean-Christophe Filliâtre. Simpler Proofs with Decentralized Invariants. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2021, 121. ⟨hal-02518570⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02518570/file/main.pdf BibTex

Conference papers

ref_biblio
Benedikt Becker, Cláudio Lourenço, Claude Marché. Explaining Counterexamples with Giant-Step Assertion Checking. F-IDE 2021 - 6th Workshop on Formal Integrated Development Environments, May 2021, Virtual, United States. ⟨hal-03217393⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03217393/file/fide.pdf BibTex

Reports

ref_biblio
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. A Coq Formalization of Lebesgue Integration of Nonnegative Functions. [Research Report] RR-9401, Inria, France. 2021, pp.37. ⟨hal-03194113⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03194113/file/RR-9401.pdf BibTex
ref_biblio
Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, et al.. Formal Analysis of Ladder Programs using Deductive Verification. [Research Report] RR-9402, Inria. 2021, pp.25. ⟨hal-03199464⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03199464/file/RR-9402.pdf BibTex
ref_biblio
Benedikt Becker, Cláudio Belo Lourenço, Claude Marché. Giant-step Semantics for the Categorisation of Counterexamples. [Research Report] RR-9407, Inria. 2021, pp.43. ⟨hal-03213438⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03213438/file/RR-9407.pdf BibTex

Preprints, Working Papers, ...

ref_biblio
Jean-Christophe Filliâtre, Clément Pascutto. Ortac: Runtime Assertion Checking for OCaml (tool paper). 2021. ⟨hal-03252901⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03252901/file/RV_2021.pdf BibTex
ref_biblio
Sylvie Boldo, Guillaume Melquiond. Some Formal Tools for Computer Arithmetic: Flocq and Gappa. 2021. ⟨hal-03233227⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03233227/file/article.pdf BibTex
ref_biblio
Guillaume Melquiond. Plotting in a Formally Verified Way. 2021. ⟨hal-03168208v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03168208/file/article.pdf BibTex
ref_biblio
Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond. A strong call-by-need calculus. 2021. ⟨hal-03149692v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03149692/file/main.pdf BibTex
ref_biblio
Andrei Paskevich. Continuation Passing as an Abstract Syntax for Deductive Verification. 2021. ⟨hal-03115120⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03115120/file/leiden.pdf BibTex

2020

Journal articles

ref_biblio
Sylvain Conchon, David Declerck, Fatiha Zaïdi. Parameterized Model Checking on the TSO Weak Memory Model. Journal of Automated Reasoning, Springer Verlag, 2020, 64 (7), pp.1307-1330. ⟨10.1007/s10817-020-09565-w⟩. ⟨hal-03149332⟩
Accès au bibtex
BibTex
ref_biblio
Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq. Optimal Inverse Projection of Floating-Point Addition. Numerical Algorithms, Springer Verlag, In press, 83 (3), pp.957--986. ⟨10.1007/s11075-019-00711-z⟩. ⟨hal-01939097⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01939097/file/main.pdf BibTex
ref_biblio
Sylvie Boldo, Christoph Lauter, Jean-Michel Muller. Emulating round-to-nearest ties-to-zero "augmented" floating-point operations using round-to-nearest ties-to-even arithmetic. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, In press, ⟨10.1109/TC.2020.3002702⟩. ⟨hal-02137968v4⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02137968/file/Emulation-RN0-revised.pdf BibTex

Conference papers

ref_biblio
Jean-Christophe Filliâtre, Andrei Paskevich. Abstraction and Genericity in Why3. ISoLA 2020 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2020, Rhodes, Greece. ⟨hal-02696246⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02696246/file/main.pdf BibTex
ref_biblio
Guillaume Melquiond, Raphaël Rieu-Helft. WhyMP, a Formally Verified Arbitrary-Precision Integer Library. ISSAC 2020 - 45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece. pp.352-359, ⟨10.1145/3373207.3404029⟩. ⟨hal-02566654v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02566654/file/main.pdf BibTex
ref_biblio
Jean-Christophe Filliâtre. a Coq retrospective - at the heart of Coq architecture, the genesis of version 7.0. The Coq Workshop 2020, Jul 2020, virtual, France. ⟨hal-02890460⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02890460/file/filliatre-coq-workshop-2020.pdf BibTex
ref_biblio
Sylvie Boldo, Diane Gallois-Wong, Thibault Hilaire. A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm. ARITH 2020 - IEEE 27th Symposium on Computer Arithmetic, Jun 2020, Portland, United States. pp.9-16, ⟨10.1109/ARITH48897.2020.00011⟩. ⟨hal-02982017⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02982017/file/paper_17.pdf BibTex
ref_biblio
Diego Diverio, Cláudio Lourenço, Claude Marché. You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3. VerifyThis 2020 - Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7. ⟨hal-03002187⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03002187/file/main.pdf BibTex
ref_biblio
Quentin Garchery, Chantal Keller, Claude Marché, Andrei Paskevich. Des transformations logiques passent leur certicat. JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. ⟨hal-02384946v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02384946/file/main.pdf BibTex
ref_biblio
Jean-Christophe Filliâtre. Mesurer la hauteur d'un arbre. JLFA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. ⟨hal-02315541v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02315541/file/main-pp.pdf BibTex
ref_biblio
Thierry Lecomte, David Déharbe, Denis Sabatier, Etienne Prun, Patrick Péronne, et al.. Low Cost High Integrity Platform: regular paper. ERTS 2020 - 10th European Congress on Embedded Real Time Systems, Jan 2020, Toulouse, France. ⟨hal-02446132⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02446132/file/Low_Cost_High_Integrity_Platform.pdf BibTex
ref_biblio
Martin Clochard, Claude Marché, Andrei Paskevich. Deductive Verification with Ghost Monitors. POPL 2020 - 47th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1145/3371070⟩. ⟨hal-02368284⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02368284/file/article.pdf BibTex
ref_biblio
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich. Verification of Programs with Pointers in SPARK. ICFEM 2020 - Formal Methods and Software Engineering, 2020, The conference took place on-line, because it couldn't be held in Singapore, Singapore. pp.55-72, ⟨10.1007/978-3-030-63406-3_4⟩. ⟨hal-03094566⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03094566/file/ICFEM20_paper_5.pdf BibTex
ref_biblio
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, et al.. Analysing installation scenarios of Debian packages. TACAS 2020 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2020, The conference took place on-line, because it couldn't be held in Dublin, Ireland. pp.235-253, ⟨10.1007/978-3-030-45237-7_14⟩. ⟨hal-02355602v2⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02355602/file/main.pdf BibTex

Books

ref_biblio
Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyen. Numérique et Sciences Informatiques, 24 leçons avec exercices corrigés. Terminale. Ellipses, pp.526, 2020, 9782340038554. ⟨hal-03023099⟩
Accès au bibtex
BibTex

Reports

ref_biblio
Xavier Denis. Deductive program verification for a language with a Rust-like typing discipline. [Internship report] Université de Paris. 2020. ⟨hal-02962804⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02962804/file/paper.pdf BibTex
ref_biblio
Benedikt Becker, Jean-Christophe Filliâtre, Claude Marché. Rapport d'avancement sur la vérification formelle des algorithmes de ParcourSup. [Rapport Technique] Université Paris-Saclay. 2020. ⟨hal-02447409⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02447409/file/main.pdf BibTex

Theses

ref_biblio
Raphaël Rieu. Development and verification of arbitrary-precision integer arithmetic libraries. Computer Arithmetic. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG023⟩. ⟨tel-03032942⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-03032942/file/93272_RIEU_2020_archivage.pdf BibTex

Preprints, Working Papers, ...

ref_biblio
Guillaume Melquiond, Raphaël Rieu-Helft. WhyMP, a Formally Verified Arbitrary-Precision Integer Library. 2020. ⟨hal-03233220⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03233220/file/main.pdf BibTex

2019

Journal articles

ref_biblio
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩. ⟨hal-01630143v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630143/file/main.pdf BibTex
ref_biblio
Raphaël Rieu-Helft. A Why3 proof of GMP algorithms. Journal of Formalized Reasoning, ASDD-AlmaDL, 2019, ⟨10.6092/issn.1972-5787/9730⟩. ⟨hal-02477578⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02477578/file/main.pdf BibTex
ref_biblio
Anastasia Volkova, Thibault Hilaire, Christoph Lauter. Arithmetic approaches for rigorous design of reliable Fixed-Point LTI filters. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, In press, pp.1-14. ⟨10.1109/TC.2019.2950658⟩. ⟨hal-01918650v2⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01918650/file/wcpg.pdf BibTex
ref_biblio
Eike Neumann, Florian Steinberg. Parametrised second-order complexity theory with applications to the study of interval computation. Theoretical Computer Science, Elsevier, In press, ⟨10.1016/j.tcs.2019.05.009⟩. ⟨hal-02148494⟩
Accès au bibtex
BibTex
ref_biblio
Sylvie Boldo, Florian Faissole, Alexandre Chapoutot. Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, In press, ⟨10.1109/TC.2019.2917902⟩. ⟨hal-01883843v3⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01883843/file/hal_article.pdf BibTex

Conference papers

ref_biblio
Jean-Christophe Filliâtre. Deductive Verification of OCaml Libraries. iFM 2019 - International Conference on integrated Formal Methods, Dec 2019, Bergen, Norway. ⟨hal-02406253⟩
Accès au bibtex
BibTex
ref_biblio
Sylvain Conchon, Mattias Roux. Reasoning about Universal Cubes in MCMT. ICFEM 2019 - 21st International Conference on Formal Engineering Methods, Nov 2019, Shenzhen, China. pp.270--285. ⟨hal-02420588⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02420588/file/main.pdf BibTex
ref_biblio
Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira. GOSPEL -Providing OCaml with a Formal Specification Language. FM 2019 - 23rd International Symposium on Formal Methods, Oct 2019, Porto, Portugal. ⟨hal-02157484v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02157484/file/final.pdf BibTex
ref_biblio
Florian Steinberg, Holger Thies, Laurent Théry. Quantitative continuity and Computable Analysis in Coq. ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.ITP.2019.28⟩. ⟨hal-02426470⟩
Accès au bibtex
BibTex
ref_biblio
Benedikt Becker, Claude Marché. Ghost Code in Action: Automated Verification of a Symbolic Interpreter. VSTTE 2019 - 11th Working Conference on Verified Software: Tools, Techniques and Experiments, Jul 2019, New York, United States. ⟨10.1007/978-3-030-41600-3_8⟩. ⟨hal-02276257⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02276257/file/Ghost_Code_in_Action_Automated_Verification_of_a_Symbolic_Interpreter.pdf BibTex
ref_biblio
Florian Faissole. Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matriciels. AFADL 2019 - 18e journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2019, Toulouse, France. ⟨hal-02391924⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02391924/file/afadlhal.pdf BibTex
ref_biblio
Guillaume Melquiond, Raphaël Rieu-Helft. Formal Verification of a State-of-the-Art Integer Square Root. ARITH-26 2019 - 26th IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.183-186, ⟨10.1109/ARITH.2019.00041⟩. ⟨hal-02092970⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02092970/file/main.pdf BibTex
ref_biblio
Thibault Hilaire, Hacène Ouzia, Benoit Lopez. Optimal Word-Length Allocation for the Fixed-Point Implementation of Linear Filters and Controllers. ARITH 2019 - IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.175-182, ⟨10.1109/ARITH.2019.00040⟩. ⟨hal-02393851⟩
Accès au texte intégral et bibtex
https://hal.sorbonne-universite.fr/hal-02393851/file/arith.pdf BibTex
ref_biblio
Cláudio Belo Lourenço, Maria Frade, Jorge Sousa Pinto. A Generalized Program Verification Workflow Based on Loop Elimination and SA Form. FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering, May 2019, Montreal, Canada. ⟨hal-02431769⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02431769/file/main.pdf BibTex
ref_biblio
Akitoshi Kawamura, Florian Steinberg, Holger Thies. Second-Order Linear-Time Computability with Applications to Computable Analysis. TAMC 2019 - 15th Annual Conference Theory and Applications of Models of Computation, Apr 2019, Tokyo, Japan. pp.337-358. ⟨hal-02148490⟩
Accès au bibtex
BibTex
ref_biblio
Raphaël Rieu-Helft. Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP. JFLA 2019 - 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Rousses, France. ⟨hal-01943010⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01943010/file/main.pdf BibTex
ref_biblio
Guillaume Melquiond. Arithmétique des Ordinateurs et Preuves Formelles. JFLA 2019 - 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. ⟨hal-02013540⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02013540/file/article.pdf BibTex
ref_biblio
Jean-Christophe Filliâtre. Retour sur 25 ans de programmation avec OCaml. JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. ⟨hal-02406208⟩
Accès au bibtex
BibTex
ref_biblio
Diane Gallois-Wong. Formalisation en Coq d'algorithmes de filtres numériques. JFLA 2019 - Journées Francophones des Langages Applicatifs, Nicolas Magaud, Jan 2019, Les Rousses, France. ⟨hal-01929531v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01929531/file/JFLA19-coq-filtres-num.pdf BibTex
ref_biblio
Valentin Blot, Amina Bousalem, Quentin Garchery, Chantal Keller. SMTCoq: automatisation expressive et extensible dans Coq. JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. ⟨hal-02369249⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02369249/file/main.pdf BibTex

Directions of work or proceedings

ref_biblio
Sylvie Boldo, Martin Langhammer. Proceedings of the 26th Symposium on Computer Arithmetic (ARITH 2019). ARITH 2019 - 26th IEEE Symposium on Computer Arithmetic, Jun 2019, Kyoto, IEEE, 2019, 978-1-7281-3367-6. ⟨10.1109/ARITH.2019.00005⟩. ⟨hal-02433652⟩
Accès au bibtex
BibTex

Habilitation à diriger des recherches

ref_biblio
Guillaume Melquiond. Formal Verification for Numerical Computations, and the Other Way Around. Computer Arithmetic. Université Paris Sud, 2019. ⟨tel-02194683⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-02194683/file/hdr.pdf BibTex

Books

ref_biblio
Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyễn. Numérique et Sciences Informatiques, 30 leçons avec exercices corrigés. Première.. Ellipses, 2019. ⟨hal-02379073⟩
Accès au bibtex
BibTex

Poster communications

ref_biblio
Florian Faissole, George Constantinides, David Thomas. Formalizing loop-carried dependencies in Coq for high-level synthesis. FCCM 2019 - 27th IEEE Symposium on Field-Programmable Custom Computing Machines, Apr 2019, San Diego, United States. ⟨hal-02391954⟩
Accès au bibtex
BibTex

Documents associated with scientific events

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

Reports

ref_biblio
Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen. Specification of UNIX Utilities. [Technical Report] ANR. 2019. ⟨hal-02321691⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02321691/file/main.pdf BibTex
ref_biblio
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Ralf Treinen. Revision 2 of CoLiS language: formal syntax, semantics, concrete and symbolic interpreters. [Technical Report] ANR. 2019. ⟨hal-02321743⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02321743/file/main.pdf BibTex
ref_biblio
Léo Andrès. Vérification par preuve formelle de propriétés fonctionnelles d'algorithme de classification. [Rapport de recherche] Université Paris Sud (Paris 11) - Université Paris Saclay. 2019. ⟨hal-02421484⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02421484/file/internship-report-parcoursup.pdf BibTex
ref_biblio
Marieke Huisman, Rosemary Monahan, Peter Müller, Andrei Paskevich, Gidon Ernst. VerifyThis 2018: A Program Verification Competition. [Research Report] Université Paris-Saclay. 2019. ⟨hal-01981937⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01981937/file/sttt-summary.pdf BibTex

Notes de synthèse

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

Preprints, Working Papers, ...

ref_biblio
Florian Steinberg, Laurent Théry, Holger Thies. Quantitative continuity and computable analysis in Coq. 2019. ⟨hal-02088293⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02088293/file/paper.pdf BibTex

2018

Journal articles

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

Conference papers

ref_biblio
Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire. A Coq formalization of digital filters. CICM 2018 - 11th Conference on Intelligent Computer Mathematics, Aug 2018, Hagenberg, Austria. pp.87--103, ⟨10.1007/978-3-319-96812-4_8⟩. ⟨hal-01728828v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01728828/file/CICM18.pdf BibTex
ref_biblio
Akitoshi Kawamura, Florian Steinberg, Holger Thies. Parameterized Complexity for Uniform Operators on Multidimensional Analytic Functions and ODE Solving. Wollic 2018 - International Workshop on Logic, Language, Information, and Computation, Jul 2018, Bogota, Colombia. pp.223-236, ⟨10.1007/978-3-662-57669-4_13⟩. ⟨hal-02019142⟩
Accès au bibtex
BibTex
ref_biblio
Guillaume Melquiond, Raphaël Rieu-Helft. A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms. 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, ⟨10.1007/978-3-319-94205-6_13⟩. ⟨hal-01699754v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01699754/file/main.pdf BibTex
ref_biblio
Sylvain Conchon, David Declerck, Fatiha Zaïdi. Cubicle-W: Parameterized Model Checking on Weak Memory. IJCAR 2018 - International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.152-160. ⟨hal-02420590⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02420590/file/paper.pdf BibTex
ref_biblio
Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, Alain Mebsout. Alt-Ergo 2.2. SMT Workshop: International Workshop on Satisfiability Modulo Theories, Jul 2018, Oxford, United Kingdom. ⟨hal-01960203⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01960203/file/Alt-Ergo-2.2--SMT-Workshop-2018.pdf BibTex
ref_biblio
Bruce Kapron, Florian Steinberg. Type-two polynomial-time and restricted lookahead. LICS 2018 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. pp.579-588, ⟨10.1145/3209108.3209124⟩. ⟨hal-02019150⟩
Accès au bibtex
BibTex
ref_biblio
Sylvie Boldo, Florian Faissole, Vincent Tourneur. A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. 25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States. ⟨hal-01772272⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01772272/file/article-HAL.pdf BibTex
ref_biblio
Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando. Parameterized Verification of Topology-sensitive Distributed Protocols goes Declarative. International Conference on Networked Systems (NETYS), May 2018, Essaouira, Morocco. ⟨hal-02001652⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02001652/file/main-2.pdf BibTex
ref_biblio
Pierre Roux, Mohamed Iguernelala, Sylvain Conchon. A Non-linear Arithmetic Procedure for Control-Command Software Verification. 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Apr 2018, Thessalonique, Greece. pp.132-151. ⟨hal-01737737⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01737737/file/submission.pdf BibTex
ref_biblio
Eike Neumann, Florian Steinberg. Parametrised second-order complexity theory with applications to the study of interval computation. DICE 2018 - Developments in Implicit Computational Complexity, Apr 2018, Thesaloniki, Greece. ⟨hal-02019134⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02019134/file/SN.pdf BibTex
ref_biblio
Jean-Christophe Filliâtre, Mário Pereira, Simão Melo de Sousa. Vérification de programmes OCaml fortement impératifs avec Why3. JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. pp.1-14. ⟨hal-01649989v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01649989/file/main.pdf BibTex
ref_biblio
Florian Faissole, Bas Spitters. Preuves constructives de programmes probabilistes. JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. ⟨hal-01654459⟩
Accès au bibtex
BibTex
ref_biblio
Raphaël Rieu-Helft. Un mécanisme d'extraction vers C pour Why3. 29èmes Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. ⟨hal-01653153⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01653153/file/main.pdf BibTex
ref_biblio
Florian Faissole. Définir le fini : deux formalisations d'espaces de dimension finie. JLFA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-mer, France. pp.1-6. ⟨hal-01654457⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01654457/file/jfla.pdf BibTex
ref_biblio
Sylvain Dailler, Claude Marché, Yannick Moy. Lightweight Interactive Proving inside an Automatic Program Verifier. 4th Workshop on Formal Integrated Development Environment, 2018, Oxford, United Kingdom. ⟨hal-01936302⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01936302/file/article.pdf BibTex

Directions of work or proceedings

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

Books

ref_biblio
Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, et al.. Handbook of Floating-point Arithmetic (2nd edition). Birkhäuser Basel, pp.1-627, 2018, 978-3319765259. ⟨10.1007/978-3-319-76526-6⟩. ⟨hal-01766584⟩
Accès au bibtex
BibTex

Patents

ref_biblio
Jean-Christophe Filliâtre, Andrei Paskevich, Guillaume Melquiond, Claude Marché, François Bobot. Why3 version 1.0. France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018. ⟨hal-03136256⟩
Accès au bibtex
BibTex

Documents associated with scientific events

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

Reports

ref_biblio
Martin Clochard, Andrei Paskevich, Claude Marché. Deductive Verification via Ghost Debugging. [Research Report] RR-9219, Inria Saclay Ile de France. 2018. ⟨hal-01907894⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01907894/file/RR-9219.pdf BibTex
ref_biblio
Quentin Garchery. Démonstration automatique en Coq. [Travaux universitaires] Paris Diderot; Laboratoire de recherche en informatique (LRI) UMR CNRS 8623, Université Paris-Sud. 2018. ⟨hal-01874777⟩
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

ref_biblio
Martin Clochard. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. Autre [cs.OH]. Université Paris Saclay (COmUE), 2018. Français. ⟨NNT : 2018SACLS071⟩. ⟨tel-01787689⟩
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, ...

ref_biblio
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich. Verification of Programs with Pointers in SPARK. 2018. ⟨hal-01936105⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01936105/file/report.pdf BibTex
ref_biblio
Martin Clochard, Claude Marché, Andrei Paskevich. Deductive Verification with Ghost Monitors. 2018. ⟨hal-01926659⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01926659/file/article.pdf BibTex

2017

Journal articles

ref_biblio
Ran Chen, Martin Clochard, Claude Marché. A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. Journal of Formalized Reasoning, ASDD-AlmaDL, 2017, 10 (1). ⟨hal-01652148⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01652148/file/jfr7213.pdf BibTex
ref_biblio
Sylvie Boldo, Stef Graillat, Jean-Michel Muller. On the robustness of the 2Sum and Fast2Sum algorithms. ACM Transactions on Mathematical Software, Association for Computing Machinery, 2017, 44 (1). ⟨ensl-01310023v2⟩
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

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

Directions of work or proceedings

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

Other publications

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

Books

ref_biblio
Sylvie Boldo, Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press - Elsevier, pp.326, 2017, 9781785481123. ⟨hal-01632617⟩
Accès au bibtex
BibTex

Poster communications

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

Reports

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

2016

Journal articles

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

Conference papers

ref_biblio
Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles. Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. 7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. pp.461--478. ⟨hal-01344110⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01344110/file/paper063.pdf BibTex
ref_biblio
Umut Acar, Arthur Charguéraud, Mike Rainey, Filip Sieczkowski. Dag-calculus: a calculus for parallel computation. Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), Sep 2016, Nara, Japan. pp.18 - 32, ⟨10.1145/2951913.2951946⟩. ⟨hal-01409022⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01409022/file/dag_calculus_icfp16.pdf BibTex
ref_biblio
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Interactive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩. ⟨hal-01289616v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01289616/file/main.pdf BibTex
ref_biblio
Sylvie Boldo. Iterators: where folds fail. Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada. ⟨hal-01377155⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01377155/file/abstract.pdf BibTex
ref_biblio
Martin Clochard, Léon Gondelman, Mário Pereira. The Matrix Reproved (Verification Pearl). VSTTE 2016, Jul 2016, Toronto, Canada. ⟨hal-01316902v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01316902/file/paper_12.pdf BibTex
ref_biblio
Jean-Christophe Filliâtre, Mário Pereira. Producing All Ideals of a Forest, Formally (Verification Pearl). VSTTE 2016, Jul 2016, Toronto, Canada. pp.46 - 55, ⟨10.1007/978-3-319-48869-1_4⟩. ⟨hal-01316859v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01316859/file/paper_6.pdf BibTex
ref_biblio
Sylvie Boldo. Computing a correct and tight rounding error bound using rounding-to-nearest. 9th International Workshop on Numerical Software Verification, Jul 2016, Toronto, Canada. ⟨hal-01377152⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01377152/file/article.pdf BibTex
ref_biblio
David Hauzar, Claude Marché, Yannick Moy. Counterexamples from Proof Failures in SPARK. Software Engineering and Formal Methods, Jul 2016, Vienna, Austria. ⟨hal-01314885⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01314885/file/article.pdf BibTex
ref_biblio
Jean-Christophe Filliâtre, Mário Pereira. A Modular Way to Reason About Iteration. 8th NASA Formal Methods Symposium, Jun 2016, Minneapolis, United States. ⟨hal-01281759v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01281759/file/main.pdf BibTex
ref_biblio
Clément Fumex, Claire Dross, Jens Gerlach, Claude Marché. Specification and Proof of High-Level Functional Properties of Bit-Level Programs. NASA Formal methods, Jun 2016, Minneapolis, United States. ⟨hal-01314876⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01314876/file/article-final.pdf BibTex
ref_biblio
Érik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq (Journées FAC 2016). Journées Formalisation des Activités Concurrentes (FAC 2016), Groupe IFSE du RTRA STAE (Réseau Thématique de Recherche Avancée « Sciences et Technologies pour l’Aéronautique et l’Espace » de Toulouse), Mar 2016, Toulouse, France. ⟨hal-03176418⟩
Accès au bibtex
BibTex
ref_biblio
Jean-Christophe Filliâtre, Mário Pereira. Itérer avec confiance. Journées Francophones des Langages Applicatifs, Jan 2016, Saint-Malo, France. ⟨hal-01240891⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01240891/file/main.pdf BibTex
ref_biblio
Arthur Charguéraud. Higher-order representation predicates in separation logic. Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), Jan 2016, St. Petersburg, FL, United States. pp.3 - 14, ⟨10.1145/2854065.2854068⟩. ⟨hal-01408670⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01408670/file/horepr.pdf BibTex
ref_biblio
Érik Martin-Dorel, Guillaume Melquiond. CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq. MAP 2016 conference on Effective Analysis: Foundations, Implementations, Certification, Jan 2016, Marseille, France. ⟨hal-03155045⟩
Accès au bibtex
BibTex

Documents associated with scientific events

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

Reports

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

Preprints, Working Papers, ...

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

2015

Journal articles

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

Conference papers

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

Book sections

ref_biblio
Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. 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. ⟨hal-01094195⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094195/file/CIC.pdf BibTex

Other publications

ref_biblio
Thierry Viéville, Sylvie Boldo, Florent Masseglia, Pierre Bernhard. « Structures : organisation, complexité, dynamique » des mot-clés au sens inattendu. 2015. ⟨hal-01238442⟩
Accès au bibtex
BibTex

Reports

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

2014

Journal articles

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

Conference papers

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

Book sections

ref_biblio
Sylvie Boldo. Même les ordinateurs font des erreurs !. 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. ⟨hal-01089095⟩
Accès au bibtex
BibTex

Habilitation à diriger des recherches

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

Books

ref_biblio
Sylvain Conchon, Jean-Christophe Filliâtre. Apprendre à programmer avec OCaml. Eyrolles, pp.429, 2014, Noire, 9782212136784. ⟨hal-01063853⟩
Accès au bibtex
BibTex

Reports

ref_biblio
Érik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions in Coq. [Research Report] IRIT-RR-2014-09-FR, IRIT : Institut de Recherche Informatique de Toulouse. 2014, pp.1-32. ⟨hal-03260617⟩
Accès au bibtex
BibTex

2013

Journal articles

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

Conference papers

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

Book sections

ref_biblio
Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. Informatique mathématique : Une photographie en 2013, 2013. ⟨hal-01767900⟩
Accès au bibtex
BibTex

Directions of work or proceedings

ref_biblio
Sandrine Blazy, Christine Paulin-Mohring, David Pichardie. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. 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⟩. ⟨hal-00908865⟩
Accès au bibtex
BibTex

Other publications

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

Books

ref_biblio
Judicaël Courant, Marc de Falco, Stéphane Gonnord, Jean-Christophe Filliâtre, Sylvain Conchon, et al.. Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python. Eyrolles, pp.1-390, 2013, 978-2-212-13700-2. ⟨hal-00880268⟩
Accès au bibtex
BibTex

Reports

ref_biblio
Umut Acar, Arthur Charguéraud, Stefan Muller, Mike Rainey. Atomic Read-Modify-Write Operations are Unnecessary for Shared-Memory Work Stealing. [Research Report] 2013. ⟨hal-00910130⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00910130/file/main.pdf BibTex
ref_biblio
Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, et al.. Médiation Scientifique : une facette de nos métiers de la recherche. [Interne] none. 2013, pp.34. ⟨hal-00804915⟩
Accès au bibtex
BibTex

Theses

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

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

2012

Journal articles

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

Conference papers

ref_biblio
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. pp.289-304, ⟨10.1007/978-3-642-35308-6_22⟩. ⟨hal-00712938v2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00712938/file/article.pdf BibTex
ref_biblio
François Bobot, Jean-Christophe Filliâtre. Separation Predicates: a Taste of Separation Logic in First-Order Logic. 14th International Conference on Formal Ingineering Methods (ICFEM), Nov 2012, Kyoto, Japan. pp.167-181, ⟨10.1007/978-3-642-34281-3_14⟩. ⟨hal-00825088⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00825088/file/bobot12icfem.pdf BibTex
ref_biblio
Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump. The 2nd Verified Software Competition: Experience Report. COMPARE 2012, Comparative Empirical Evaluation of Reasoning Systems, 1st Intl. Workshop, Jun 2012, Manchester, United Kingdom. pp.36-49. ⟨hal-00798777⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00798777/file/main.pdf BibTex
ref_biblio
Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala. Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. 10th International Workshop on Satisfiability Modulo Theories, Jun 2012, Manchester, United Kingdom. pp.12-21. ⟨hal-01785166⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01785166/file/article.pdf BibTex
ref_biblio
Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. École des Jeunes Chercheurs en Informatique Mathématique, GDR Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30. ⟨hal-00755333⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00755333/file/main.pdf BibTex

2011

Conference papers

ref_biblio
Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst, Jean-Christophe Filliâtre, et al.. The COST IC0701 Verification Competition 2011. Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, 2011, Torino, Italy. ⟨hal-00789525⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00789525/file/costcomp2011.pdf BibTex

2010

Journal articles

ref_biblio
Sylvie Boldo. Un algorithme de découpe de gâteau. Interstices, INRIA, 2010. ⟨hal-01350225⟩
Accès au bibtex
BibTex

Conference papers

ref_biblio
Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, Guillaume von Tokarski. Real-Time Monitoring of Ocaml programs. JFLA 2010, Jan 2010, Vieux-Port La Ciotat, France. pp.159-185. ⟨hal-00941407⟩
Accès au bibtex
BibTex

2009

Journal articles

ref_biblio
Sylvie Boldo. Demandez le programme. Interstices, INRIA, 2009. ⟨hal-01350274⟩
Accès au bibtex
BibTex

2008

Journal articles

ref_biblio
Sylvie Boldo, Thierry Viéville. Idée reçue : L’informatique, ce n’est pas pour les filles. Interstices, INRIA, 2008. ⟨hal-01350416⟩
Accès au bibtex
BibTex
ref_biblio
Sylvie Boldo, Joanna Jongwane. Pourquoi mon ordinateur calcule-t-il faux ?. Interstices, INRIA, 2008. ⟨hal-01350419⟩
Accès au bibtex
BibTex

2005

Conference papers

ref_biblio
Évelyne Contejean, Pierre Corbineau. Reflecting Proofs in First-Order Logic with Equality. 20th International Conference on Automated Deduction (CADE-20), 2005, Tallinn, Estonia. pp.7--22, ⟨10.1007/11532231_2⟩. ⟨hal-00946061⟩
Accès au bibtex
BibTex

2000

Reports

ref_biblio
Jean-Christophe Filliâtre. Design of a proof assistant: Coq version 7. [Research Report] Université Paris-Sud. 2000. ⟨hal-02890416⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02890416/file/coqv7.pdf BibTex