2024
Conference papers
- titre
- Alias : pointeurs espionnés en série
- auteur
- Tristan Le Gall, Jan Rochel, Florian Faissole, Julien Signoles, Denis Cousineau
- article
- 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France. pp.85-104
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation
- auteur
- Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond
- article
- 2024
- Accès au texte intégral et bibtex
-
2023
Conference papers
- titre
- Slimmer Formal Proofs for Mathematical Libraries
- auteur
- Paul Geneau de Lamarlière, Guillaume Melquiond, Florian Faissole
- article
- 30th IEEE International Symposium on Computer Arithmetic, Sep 2023, Portland (Oregon), United States. pp.4
- Accès au texte intégral et bibtex
-
Reports
- titre
- Formally Verified Bounds on Rounding Errors in Concrete Implementations of Logarithm-Sum-Exponential Functions
- auteur
- Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft
- article
- RR-9531, Inria. 2023
- Accès au texte intégral et bibtex
-
2022
Journal articles
- titre
- Automated Formal Analysis of Temporal Properties of Ladder Programs
- auteur
- Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
- article
- International Journal on Software Tools for Technology Transfer, 2022, 24 (6), pp.977-997. ⟨10.1007/s10009-022-00680-0⟩
- Accès au texte intégral et bibtex
-
- titre
- A Coq Formalization of Lebesgue Integration of Nonnegative Functions
- auteur
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
- article
- Journal of Automated Reasoning, 2022, 66, pp.175-213. ⟨10.1007/s10817-021-09612-0⟩
- Accès au texte intégral et bibtex
-
2021
Conference papers
- titre
- Automated Verification of Temporal Properties of Ladder Programs
- auteur
- Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
- article
- FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩
- Accès au texte intégral et bibtex
-
Reports
- titre
- A Coq Formalization of Lebesgue Integration of Nonnegative Functions
- auteur
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
- article
- [Research Report] RR-9401, Inria, France. 2021, pp.38
- Accès au texte intégral et bibtex
-
- titre
- Formal Analysis of Ladder Programs using Deductive Verification
- auteur
- Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
- article
- [Research Report] RR-9402, Inria. 2021, pp.25
- Accès au texte intégral et bibtex
-
2019
Journal articles
- titre
- Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods
- auteur
- Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
- article
- IEEE Transactions on Computers, 2019, ⟨10.1109/TC.2019.2917902⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matriciels
- auteur
- Florian Faissole
- article
- AFADL 2019 - 18e journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2019, Toulouse, France
- Accès au texte intégral et bibtex
-
Poster communications
- titre
- Formalizing loop-carried dependencies in Coq for high-level synthesis
- auteur
- Florian Faissole, George Constantinides, David Thomas
- article
- FCCM 2019 - 27th IEEE Symposium on Field-Programmable Custom Computing Machines, Apr 2019, San Diego, United States
- Accès au bibtex
-
Theses
- titre
- Formalisations d’analyses d’erreurs en analyse numérique et en arithmétique à virgule flottante
- auteur
- Florian Faissole
- article
- Logique en informatique [cs.LO]. Université Paris Saclay (COmUE), 2019. Français. ⟨NNT : 2019SACLS594⟩
- Accès au texte intégral et bibtex
-
2018
Conference papers
- titre
- A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers
- auteur
- Sylvie Boldo, Florian Faissole, Vincent Tourneur
- article
- 25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States
- Accès au texte intégral et bibtex
-
- titre
- Preuves constructives de programmes probabilistes
- auteur
- Florian Faissole, Bas Spitters
- article
- JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
- Accès au bibtex
-
- titre
- Définir le fini : deux formalisations d'espaces de dimension finie
- auteur
- Florian Faissole
- article
- JLFA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-mer, France. pp.1-6
- Accès au texte intégral et bibtex
-
2017
Conference papers
- titre
- Formalization and closedness of finite dimensional subspaces
- auteur
- Florian Faissole
- article
- SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
- Accès au texte intégral et bibtex
-
- titre
- Round-off Error Analysis of Explicit One-Step Numerical Integration Methods
- auteur
- Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
- article
- 24th IEEE Symposium on Computer Arithmetic, Jul 2017, London, United Kingdom. ⟨10.1109/ARITH.2017.22⟩
- Accès au texte intégral et bibtex
-
- titre
- Preuve formelle du théorème de Lax–Milgram
- auteur
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
- article
- 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France
- Accès au texte intégral et bibtex
-
- titre
- Synthetic topology in HoTT for probabilistic programming
- auteur
- Florian Faissole, Bas Spitters
- article
- The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Jan 2017, Paris, France
- Accès au bibtex
-
- titre
- A Coq formal proof of the Lax–Milgram theorem
- auteur
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
- article
- 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩
- Accès au texte intégral et bibtex
-
Poster communications
- titre
- Synthetic topology in homotopy type theory for probabilistic programming
- auteur
- Florian Faissole, Bas Spitters
- article
- PPS 2017 - Workshop on probabilistic programming semantics , Jan 2017, Paris, France. pp.3
- Accès au bibtex
-