Publications HAL de la structure toccata

2024

Conference papers

ref_biblio: Claude Marché, Denis Cousineau. De l'avantage de nuancer les décisions binaires. JFLA 2024 – 35es Journées Francophones des Langages Applicatifs, Jan 2024, Saint-Jacut-de-la-Mer, France. ⟨hal-04342273v2⟩
Accès au texte intégral et bibtex

ref_biblio: François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével. Thunks and Debits in Separation Logic with Time Credits. POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages, SIGPLAN, Jan 2024, Londres, United Kingdom. ⟨hal-04238691v2⟩
Accès au texte intégral et bibtex

ref_biblio: Amin Timany, Armaël Guéneau, Lars Birkedal. The Logical Essence of Well-Bracketed Control Flow. POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages, SIGPLAN, Jan 2024, Londres, United Kingdom. ⟨hal-04271457⟩
Accès au texte intégral et bibtex

Book sections

ref_biblio: Allan Blanchard, Claude Marché, Virgile Prévosto. Formally Expressing what a Program Should Do: the ACSL Language. Nikolai Kosmatov; Julien Signoles. Guide to Software Verification with Frama-C - Core Components, Usages, and Applications, Springer, 2024. ⟨hal-04265707⟩
Accès au bibtex

Reports

ref_biblio: Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin. Teaching Divisibility and Binomials with Coq. RR-9547, Inria. 2024, pp.13. ⟨hal-04550762⟩
Accès au texte intégral et bibtex

ref_biblio: Denis Cousineau, Hiroaki Inoue, Claude Marché, David Mentré. A Methodological Guide for the Validation of Logic Modelling of Ladder Instructions. RT-0522, Inria. 2024. ⟨hal-04487766⟩
Accès au texte intégral et bibtex

ref_biblio: Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, et al.. ANSI/ISO C Specification Language Version 1.20. CEA List. 2024. ⟨hal-04523865⟩
Accès au bibtex

Preprints, Working Papers, ...

ref_biblio: Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond. End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation. 2024. ⟨hal-04515714⟩
Accès au texte intégral et bibtex

2023

Journal articles

ref_biblio: Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux. Enabling Floating-Point Arithmetic in the Coq Proof Assistant. Journal of Automated Reasoning, 2023, 67 (33), ⟨10.1007/s10817-023-09679-x⟩. ⟨hal-04114233v2⟩
Accès au texte intégral et bibtex

ref_biblio: Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, et al.. Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. Journal of the ACM (JACM), 2023, ⟨10.1145/3623510⟩. ⟨hal-03826854v3⟩
Accès au texte intégral et bibtex

ref_biblio: Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller. Floating-point arithmetic. Acta Numerica, 2023, 32, pp.203-290. ⟨10.1017/S0962492922000101⟩. ⟨hal-04095151⟩
Accès au texte intégral et bibtex

ref_biblio: Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond. A strong call-by-need calculus. Logical Methods in Computer Science, 2023, 19 (1), pp.39. ⟨10.46298/lmcs-19(1:21)2023⟩. ⟨hal-03409681v3⟩
Accès au texte intégral et bibtex

ref_biblio: Guillaume Melquiond, Raphaël Rieu-Helft. WhyMP, a Formally Verified Arbitrary-Precision Integer Library. Journal of Symbolic Computation, 2023, 115, pp.74-95. ⟨10.1016/j.jsc.2022.07.007⟩. ⟨hal-03233220⟩
Accès au texte intégral et bibtex

ref_biblio: Sylvie Boldo, Nicolas Brisebarre, Jean-Michel Muller. Le dilemme du fabricant de tables. La Recherche, 2023, 572. ⟨hal-03932037⟩
Accès au bibtex

Conference papers

ref_biblio: Sylvain Conchon, Alexandrina Korneva. The Cubicle Fuzzy Loop: A Fuzzing-Based Extension for the Cubicle Model Checker. SEFM 2023 - Software Engineering and Formal Methods, Nov 2023, Eindhoven, Netherlands. pp.30-46, ⟨10.1007/978-3-031-47115-5_3⟩. ⟨hal-04394062v2⟩
Accès au texte intégral et bibtex

ref_biblio: Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, et al.. Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. OOPSLA 2023 - Object-Oriented Programming, Systems, Languages & Applications 2023, SIGPLAN, Oct 2023, Cascais, Portugal. ⟨10.1145/3622823⟩. ⟨hal-04203298v2⟩
Accès au texte intégral et bibtex

ref_biblio: Paul Geneau de Lamarlière, Guillaume Melquiond, Florian Faissole. Slimmer Formal Proofs for Mathematical Libraries. 30th IEEE International Symposium on Computer Arithmetic, Sep 2023, Portland (Oregon), United States. pp.4. ⟨hal-04165169⟩
Accès au texte intégral et bibtex

ref_biblio: Léo Andrès, Pierre Chambart, Jean-Christophe Filliâtre. Wasocaml: compiling OCaml to WebAssembly. IFL 2023 - The 35th Symposium on Implementation and Application of Functional Languages, João Saraiva; João Fernandes, Aug 2023, Braga, Portugal. ⟨hal-04311345v2⟩
Accès au texte intégral et bibtex

ref_biblio: Assia Mahboubi, Guillaume Melquiond. Manifest Termination. TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-3. ⟨hal-04172297⟩
Accès au texte intégral et bibtex

ref_biblio: Xavier Denis, Jacques-Henri Jourdan. Specifying and Verifying Higher-order Rust Iterators. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), ETAPS, Apr 2023, Paris, France. pp.93-110, ⟨10.1007/978-3-031-30820-8_9⟩. ⟨hal-03827702v2⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Christophe Filliâtre. Why3, une plateforme pour la vérification déductive. Journées FAC 2023, groupe IFSE du RTRA STAE, Apr 2023, Toulouse, France. ⟨hal-04060570⟩
Accès au texte intégral et bibtex

ref_biblio: Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. 25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.39--55, ⟨10.1007/978-3-031-27481-7_4⟩. ⟨hal-03889276v2⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Christophe Filliâtre, Andrei Paskevich. L'arithmétique de séparation. JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.274-283. ⟨hal-03886759v2⟩
Accès au texte intégral et bibtex

ref_biblio: Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, et al.. Compositional pre-processing for automated reasoning in dependent type theory. CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩. ⟨hal-03901019v3⟩
Accès au texte intégral et bibtex

Lectures

ref_biblio: Jean-Christophe Filliâtre. Structures de données semi-persistantes. Doctorat. Séminaire du cours Structures de données persistantes (Xavier Leroy, chaire Sciences du logiciel), Collège de France, France. 2023. ⟨hal-04055882⟩
Accès au texte intégral et bibtex

Reports

ref_biblio: Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft. Formally Verified Bounds on Rounding Errors in Concrete Implementations of Logarithm-Sum-Exponential Functions. RR-9531, Inria. 2023. ⟨hal-04343157v2⟩
Accès au texte intégral et bibtex

ref_biblio: Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. Lebesgue Induction and Tonelli's Theorem in Coq. [Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2023, pp.17. ⟨hal-03564379v2⟩
Accès au texte intégral et bibtex

Preprints, Working Papers, ...

ref_biblio: Josué Moreau, Guillaume Melquiond. A Safe Low-level Language for Computer Algebra and its Formally Verified Compiler. 2023. ⟨hal-04485670⟩
Accès au texte intégral et bibtex

ref_biblio: Andrei Paskevich. Flexible Verification Conditions with Continuations and Barriers. 2023. ⟨hal-04115885v3⟩
Accès au texte intégral et bibtex

2022

Journal articles

ref_biblio: Louise Ben Salem-Knapp, Sylvie Boldo, William Weens. Bounding the Round-Off Error of the Upwind Scheme for Advection. IEEE Transactions on Emerging Topics in Computing, 2022, 10 (3), ⟨10.1109/TETC.2022.3191472⟩. ⟨hal-03329933⟩
Accès au texte intégral et bibtex

ref_biblio: Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, et al.. Automated Formal Analysis of Temporal Properties of Ladder Programs. International Journal on Software Tools for Technology Transfer, 2022, 24 (6), pp.977-997. ⟨10.1007/s10009-022-00680-0⟩. ⟨hal-03737869⟩
Accès au texte intégral et bibtex

ref_biblio: Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. A Coq Formalization of Lebesgue Integration of Nonnegative Functions. Journal of Automated Reasoning, 2022, 66, pp.175-213. ⟨10.1007/s10817-021-09612-0⟩. ⟨hal-03471095⟩
Accès au texte intégral et bibtex

ref_biblio: Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, et al.. The CoLiS Platform for the Analysis of Maintainer Scripts in Debian Software Packages. International Journal on Software Tools for Technology Transfer, 2022. ⟨hal-03737886⟩
Accès au texte intégral et bibtex

Conference papers

ref_biblio: Xavier Denis, Jacques-Henri Jourdan, Claude Marché. Creusot: a Foundry for the Deductive Verification of Rust Programs. ICFEM 2022 - 23th International Conference on Formal Engineering Methods, Oct 2022, Madrid, Spain. ⟨hal-03737878⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Christophe Filliâtre, Clément Pascutto. Optimizing Prestate Copies in Runtime Verification of Function Postconditions. RV 2022 - 22nd International Conference on Runtime Verification, Sep 2022, Tbilisi, Georgia. ⟨hal-03690675v2⟩
Accès au texte intégral et bibtex

ref_biblio: Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, et al.. Proving full-system security properties under multiple attacker models on capability machines. CSF 2022 - 35th IEEE Computer Security Foundations Symposium, Aug 2022, Haifa, Israel. ⟨hal-03826851⟩
Accès au texte intégral et bibtex

ref_biblio: Léo Andrès, Raja Boujbel, Louis Gesbert, Dario Pinto. Connecter l'écosystème OCaml à Software Heritage via opam. 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.227-234. ⟨hal-03626845⟩
Accès au texte intégral et bibtex

ref_biblio: Çagdas Bozman, Mohamed Iguernlala, Michael Laporte, Maxime Levillain, Alain Mebsout, et al.. Jouez à Faire Consensus Avec MITTEN (démonstration). 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.248-250. ⟨hal-03626847⟩
Accès au texte intégral et bibtex

ref_biblio: Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. PLDI 2022 - 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2022, San Diego CA USA, United States. pp.841-856, ⟨10.1145/3519939.3523704⟩. ⟨hal-03777103⟩
Accès au texte intégral et bibtex

Books

ref_biblio: Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyen, Laurent Sartre. Informatique - MP2I/MPI - CPGE 1re et 2e années - Cours et exercices corrigés. Ellipses, pp.1116, 2022, 9782340070349. ⟨hal-03886751⟩
Accès au bibtex

Reports

ref_biblio: Sylvie Boldo, François Clément, Louise Leclerc. A Coq Formalization of the Bochner integral. [Research Report] RR-9456, Inria Saclay - Île de France; Inria de Paris. 2022. ⟨hal-03516749v2⟩
Accès au texte intégral et bibtex

Theses

ref_biblio: Quentin Garchery. Certification de la transformation de tâches de preuve. Logique en informatique [cs.LO]. Université Paris-Saclay, 2022. Français. ⟨NNT : 2022UPASG006⟩. ⟨tel-03560564⟩
Accès au texte intégral et bibtex

Preprints, Working Papers, ...

ref_biblio: Josué Moreau. Compilation formellement vérifiée d'un langage pour le calcul formel. 2022. ⟨hal-03824148⟩
Accès au texte intégral et bibtex

ref_biblio: Andrei Paskevich. Continuation Passing as an Abstract Syntax for Deductive Verification. 2022. ⟨hal-03115120v2⟩
Accès au texte intégral et bibtex

2021

Journal articles

ref_biblio: Sylvie Boldo, Christoph Q. 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, 2021, 70 (7), pp.1046 - 1058. ⟨10.1109/TC.2020.3002702⟩. ⟨hal-02137968v4⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Christophe Filliâtre. Simpler Proofs with Decentralized Invariants. Journal of Logical and Algebraic Methods in Programming, 2021, 121, ⟨10.1016/j.jlamp.2021.100645⟩. ⟨hal-02518570⟩
Accès au texte intégral et bibtex

ref_biblio: Florian Steinberg, Laurent Théry, Holger Thies. Computable analysis and notions of continuity in Coq. Logical Methods in Computer Science, 2021, 17 (2), ⟨10.23638/LMCS-17(2:16)2021⟩. ⟨hal-03324295⟩
Accès au bibtex

Conference papers

ref_biblio: Jean-Christophe Filliâtre, Andrei Paskevich. Abstraction and Genericity in Why3. ISoLA 2021 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2021, Rhodes, Greece. ⟨10.1007/978-3-030-61362-4_7⟩. ⟨hal-02696246v2⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Christophe Filliâtre, Clément Pascutto. Ortac: Runtime Assertion Checking for OCaml. RV'21 - 21st International Conference on Runtime Verification, Oct 2021, Los Angeles, CA, United States. ⟨hal-03252901v2⟩
Accès au texte intégral et bibtex

ref_biblio: Nicolas Osborne, Clément Pascutto. Leveraging Formal Specifications to Generate Fuzzing Suites. OCaml Users and Developers Workshop, co-located with the 26th ACM SIGPLAN International Conference on Functional Programming, Aug 2021, Virtual, United States. ⟨hal-03328646⟩
Accès au texte intégral et bibtex

ref_biblio: Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, et al.. Automated Verification of Temporal Properties of Ladder Programs. FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩. ⟨hal-03281580⟩
Accès au texte intégral et bibtex

ref_biblio: William Weens, Thibaud Vazquez-Gonzalez, Louise Ben Salem-Knapp. Modeling round-off errors in hydrodynamic simulations. NSV 2021 - 14th International Workshop on Numerical Software Verification, Jul 2021, Los Angeles, United States. ⟨hal-03351754⟩
Accès au texte intégral et bibtex

ref_biblio: Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond. A strong call-by-need calculus. FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires, Argentina. pp.1-22, ⟨10.4230/LIPIcs.FSCD.2021.9⟩. ⟨hal-03149692v2⟩
Accès au texte intégral et bibtex

ref_biblio: Louise Ben Salem-Knapp, Thibaud Vazquez-Gonzalez, William Weens. La double précision suffit-elle à l'exascale ?. AFADL 2021 - 20èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2021, Vannes, France. ⟨hal-03351615⟩
Accès au texte intégral et bibtex

ref_biblio: Sylvie Boldo, Guillaume Melquiond. Some Formal Tools for Computer Arithmetic: Flocq and Gappa. ARITH 2021 - 28th IEEE International Symposium on Computer Arithmetic, Jun 2021, Online, Italy. ⟨hal-03233227⟩
Accès au texte intégral et bibtex

ref_biblio: Guillaume Melquiond. Plotting in a Formally Verified Way. Proceedings of the 6th Workshop on Formal Integrated Development Environment, May 2021, Online, United States. pp.39-45, ⟨10.4204/EPTCS.338.6⟩. ⟨hal-03168208v2⟩
Accès au texte intégral et bibtex

ref_biblio: Benedikt Becker, Cláudio Belo 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. ⟨10.4204/EPTCS.338.10⟩. ⟨hal-03217393⟩
Accès au texte intégral et bibtex

ref_biblio: Quentin Garchery. A Framework for Proof-carrying Logical Transformations. Proof eXchange for Theorem Proving, 2021, Virtual, United States. pp.5-23, ⟨10.4204/EPTCS.336.2⟩. ⟨hal-03349223⟩
Accès au bibtex

Reports

ref_biblio: Xavier Denis, Jacques-Henri Jourdan, Claude Marché. The CREUSOT Environment for the Deductive Verification of Rust Programs. [Research Report] RR-9448, Inria Saclay - Île de France. 2021. ⟨hal-03526634v2⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Christophe Filliâtre. Compte-rendu de fin de projet ANR-15-CE25-0008 "VOCaL" : Programme CE25 2015. [Rapport de recherche] LMF - Laboratoire Méthodes Formelles. 2021. ⟨hal-03326775⟩
Accès au texte intégral et 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

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.38. ⟨hal-03194113v2⟩
Accès au texte intégral et 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

Theses

ref_biblio: Diane Gallois-Wong. Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie. Traitement du signal et de l'image [eess.SP]. Université Paris-Saclay, 2021. Français. ⟨NNT : 2021UPASG016⟩. ⟨tel-03202580⟩
Accès au texte intégral et 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, 2020, 64 (7), pp.1307-1330. ⟨10.1007/s10817-020-09565-w⟩. ⟨hal-03149332⟩
Accès au bibtex

ref_biblio: Anastasia Volkova, Thibault Hilaire, Christoph Lauter. Arithmetic approaches for rigorous design of reliable Fixed-Point LTI filters. IEEE Transactions on Computers, 2020, 69 (4), pp.489 - 504. ⟨10.1109/TC.2019.2950658⟩. ⟨hal-01918650v2⟩
Accès au texte intégral et bibtex

ref_biblio: Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq. Optimal Inverse Projection of Floating-Point Addition. Numerical Algorithms, In press, 83 (3), pp.957--986. ⟨10.1007/s11075-019-00711-z⟩. ⟨hal-01939097⟩
Accès au texte intégral et bibtex

Conference papers

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

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

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

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, Apr 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

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

ref_biblio: Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich. Verification of Programs with Pointers in SPARK. ICFEM 2020 - 22nd International Conference on Formal Engineering Methods, Mar 2020, Singapore / Virtual, Singapore. pp.55-72, ⟨10.1007/978-3-030-63406-3_4⟩. ⟨hal-03094566⟩
Accès au texte intégral et bibtex

ref_biblio: Quentin Garchery, Chantal Keller, Claude Marché, Andrei Paskevich. Des transformations logiques passent leur certificat. JFLA 2020 - Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. ⟨hal-02384946v2⟩
Accès au texte intégral et 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

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

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

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

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

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

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

Preprints, Working Papers, ...

ref_biblio: Jean-Christophe Filliâtre, Léon Gondelman, Cláudio Lourenço, Andrei Paskevich, Mário Pereira, et al.. A Toolchain to Produce Verified OCaml Libraries. 2020. ⟨hal-01783851v2⟩
Accès au texte intégral et bibtex

2019

Journal articles

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, 2019, 68 (4), pp.597 - 608. ⟨10.1109/TC.2018.2879432⟩. ⟨hal-01561052v3⟩
Accès au texte intégral et bibtex

ref_biblio: Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Journal of Automated Reasoning, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩. ⟨hal-01630143v2⟩
Accès au texte intégral et bibtex

ref_biblio: Eike Neumann, Florian Steinberg. Parametrised second-order complexity theory with applications to the study of interval computation. Theoretical Computer Science, In press, ⟨10.1016/j.tcs.2019.05.009⟩. ⟨hal-02148494⟩
Accès au bibtex

ref_biblio: Raphaël Rieu-Helft. A Why3 proof of GMP algorithms. Journal of Formalized Reasoning, 2019, ⟨10.6092/issn.1972-5787/9730⟩. ⟨hal-02477578⟩
Accès au texte intégral et 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, 2019, ⟨10.1109/TC.2019.2917902⟩. ⟨hal-01883843v3⟩
Accès au texte intégral et 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

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

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

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

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

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

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

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

ref_biblio: Cláudio Belo Lourenço, Maria João 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theses

ref_biblio: Mattias Roux. Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories. Logique en informatique [cs.LO]. Université Paris Saclay (COmUE), 2019. Français. ⟨NNT : 2019SACLS582⟩. ⟨tel-02496033⟩
Accès au texte intégral et bibtex

ref_biblio: Albin Coquereau. [ErgoFast] Amélioration de performances du solveur SMT Alt-Ergo grâce à l’intégration d’un solveur SAT efficace. Informatique et langage [cs.CL]. Université Paris-Saclay, 2019. Français. ⟨NNT : 2019SACLY007⟩. ⟨tel-02504894⟩
Accès au texte intégral et bibtex

ref_biblio: Florian Faissole. Formalisations d’analyses d’erreurs en analyse numérique et en arithmétique à virgule flottante. Logique en informatique [cs.LO]. Université Paris Saclay (COmUE), 2019. Français. ⟨NNT : 2019SACLS594⟩. ⟨tel-02470728⟩
Accès au texte intégral et 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

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, 2018, 99, pp.97-113. ⟨hal-01802488⟩
Accès au texte intégral et bibtex

ref_biblio: Martin Clochard, Léon Gondelman, Mário Pereira. The Matrix Reproved: Verification Pearl. Journal of Automated Reasoning, 2018, 60 (3), pp.365-383. ⟨10.1007/s10817-017-9436-2⟩. ⟨hal-01617437⟩
Accès au texte intégral et bibtex

Conference papers

ref_biblio: Jean-Christophe Filliâtre. Parcours d'un informaticien. Séminaires Pour Tous, École Normale Supérieure - Paris, Sep 2018, Paris, France. ⟨hal-04524016⟩
Accès au texte intégral et bibtex

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Documents associated with scientific events

ref_biblio: Christine Gassner, 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

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

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

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

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

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

ref_biblio: Martin Clochard, Claude Marché, Andrei Paskevich. Deductive Verification with Ghost Monitors. 2018. ⟨hal-01926659⟩
Accès au texte intégral et 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, 2017, 10 (1). ⟨hal-01652148⟩
Accès au texte intégral et bibtex

ref_biblio: Sylvie Boldo, Stef Graillat, Jean-Michel Muller. On the robustness of the 2Sum and Fast2Sum algorithms. ACM Transactions on Mathematical Software, 2017, 44 (1). ⟨ensl-01310023v2⟩
Accès au texte intégral et 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Special issue

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

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

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

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

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

Proceedings

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

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

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

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

2016

Journal articles

ref_biblio: Umut A Acar, Arthur Charguéraud, Mike Rainey. Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages. Journal of Functional Programming, 2016, 26, ⟨10.1017/S0956796816000101⟩. ⟨hal-01409069⟩
Accès au texte intégral et 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, 2016, 26 (7), pp.1196-1233. ⟨10.1017/S0960129514000437⟩. ⟨hal-00806920v2⟩
Accès au texte intégral et bibtex

ref_biblio: Érik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. Journal of Automated Reasoning, 2016, 57 (3), pp.187-217. ⟨10.1007/s10817-015-9350-4⟩. ⟨hal-01086460v2⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. The Spirit of Ghost Code. Formal Methods in System Design, 2016, 48 (3), pp.152-174. ⟨10.1007/s10703-016-0243-x⟩. ⟨hal-01396864⟩
Accès au texte intégral et 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, 2016, 56 (4), pp.387-457. ⟨10.1007/s10817-015-9352-2⟩. ⟨hal-01221066⟩
Accès au texte intégral et 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

ref_biblio: Umut A 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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, 2015, 9 (1), pp.41-62. ⟨10.1007/s11786-014-0181-1⟩. ⟨hal-00860648v2⟩
Accès au texte intégral et bibtex

ref_biblio: Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩. ⟨hal-00862689v3⟩
Accès au texte intégral et bibtex

ref_biblio: Claude Marché, Johannes Kanig. Bridging the Gap between Testing and Formal Verification in Ada Development. ERCIM News, 2015, 100, pp.2. ⟨hal-01102242⟩
Accès au bibtex

ref_biblio: François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Let's Verify This with Why3. International Journal on Software Tools for Technology Transfer, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩. ⟨hal-00967132⟩
Accès au texte intégral et 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, 2015, 54 (1), pp.1-29. ⟨10.1007/s10817-014-9312-2⟩. ⟨hal-00919498v2⟩
Accès au texte intégral et bibtex

ref_biblio: Pierre Roux. Formal Proofs of Rounding Error Bounds: With application to an automatic positive definiteness check. Journal of Automated Reasoning, 2015, pp.23. ⟨10.1007/s10817-015-9339-z⟩. ⟨hal-01091189v2⟩
Accès au texte intégral et 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

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

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

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

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

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

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

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

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

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

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

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

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

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

2014

Journal articles

ref_biblio: Pierre Roux. Innocuous Double Rounding of Basic Arithmetic Operations. Journal of Formalized Reasoning, 2014, 7 (1), pp.131-142. ⟨10.6092/issn.1972-5787/4359⟩. ⟨hal-01091186⟩
Accès au texte intégral et bibtex

ref_biblio: Jean-Michel Muller, Sylvie Boldo. Des ordinateurs capables de calculer plus juste. La Recherche, 2014, pp.46-53. ⟨ensl-01069744⟩
Accès au 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, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩. ⟨hal-00769201v3⟩
Accès au texte intégral et bibtex

ref_biblio: Claude Marché. Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study. Science of Computer Programming, 2014, 93 (3), pp.279-296. ⟨10.1016/j.scico.2014.04.003⟩. ⟨hal-00967124⟩
Accès au texte intégral et 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2013

Journal articles

ref_biblio: Érik Martin-Dorel, Guillaume Melquiond, Jean-Michel Muller. Some issues related to double roundings. BIT Numerical Mathematics, 2013, 53 (4), pp.897-924. ⟨10.1007/s10543-013-0436-2⟩. ⟨ensl-00644408v3⟩
Accès au texte intégral et 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, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩. ⟨hal-00649240v3⟩
Accès au texte intégral et bibtex

ref_biblio: Guillaume Melquiond, Werner Georg Nowak, Paul Zimmermann. Numerical Approximation of the Masser-Gramain Constant to Four Decimal Digits: delta=1.819.... Mathematics of Computation, 2013, 82, pp.1235-1246. ⟨10.1090/S0025-5718-2012-02635-4⟩. ⟨hal-00644166⟩
Accès au 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

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

ref_biblio: Guillaume Melquiond. Automations for verifying floating-point algorithms. 5th Coq Workshop, Jul 2013, Rennes, France. ⟨hal-01110666⟩
Accès au 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

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

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

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

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

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

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

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

ref_biblio: Umut A. 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

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

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

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

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

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

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

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

ref_biblio: Sandrine Blazy, Christine Paulin-Mohring, David Pichardie (Dir.). Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Springer, 7998, pp.500, 2013, Lecture Notes in Computer Science, ⟨10.1007/978-3-642-39634-2⟩. ⟨hal-00908865⟩
Accès au bibtex

Reports

ref_biblio: Umut A. 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

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] Inria. 2013, pp.34. ⟨hal-00804915⟩
Accès au texte intégral et 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

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

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

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

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

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

2012

Journal articles

ref_biblio: Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 2012, 216, pp.14-23. ⟨10.1016/j.ic.2011.09.005⟩. ⟨hal-00797913⟩
Accès au texte intégral et 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

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

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

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

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

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

2010

Journal articles

ref_biblio: Sylvie Boldo. Un algorithme de découpe de gâteau. Interstices, 2010. ⟨hal-01350225⟩
Accès au 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

2009

Journal articles

ref_biblio: Sylvie Boldo. Demandez le programme. Interstices, 2009. ⟨hal-01350274⟩
Accès au 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, 2008. ⟨hal-01350416⟩
Accès au bibtex

ref_biblio: Sylvie Boldo, Joanna Jongwane. Pourquoi mon ordinateur calcule-t-il faux ?. Interstices, 2008. ⟨hal-01350419⟩
Accès au 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

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