Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. - Sylvie Boldo; Florian Faissole; Alexandre Chapoutot (ARITH, 2017)

A Coq formal proof of the LaxMilgram theorem. - Sylvie Boldo; François Clément; Florian Faissole; Vincent Martin; Micaela Mayero (CPP, 2017)

Formalization and Closedness of Finite Dimensional Subspaces. - Florian Faissole (SYNASC, 2017)

A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. - Sylvie Boldo; Florian Faissole; Vincent Tourneur (ARITH, 2018)

Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis. - Florian Faissole; George A. Constantinides; David B. Thomas (FCCM, 2019)

Formalisations d'analyses d'erreurs en analyse numérique et en arithmétique à virgule flottante. (Formalizations of error analysis in numerical analysis and floating-point arithmetic). - Florian Faissole (2019)

Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods. - Sylvie Boldo; Florian Faissole; Alexandre Chapoutot (IEEE Trans. Computers, 2020)

Automated Verification of Temporal Properties of Ladder Programs. - Cláudio Belo Lourenço; Denis Cousineau 002; Florian Faissole; Claude Marché; David Mentré; Hiroaki Inoue (FMICS, 2021)

Synthetic topology in Homotopy Type Theory for probabilistic programming. - Martin E. Bidlingmaier; Florian Faissole; Bas Spitters (Math. Struct. Comput. Sci., 2021)

A Coq Formalization of Lebesgue Integration of Nonnegative Functions. - Sylvie Boldo; François Clément; Florian Faissole; Vincent Martin; Micaela Mayero (J. Autom. Reason., 2022)

Automated formal analysis of temporal properties of Ladder programs. - Cláudio Belo Lourenço; Denis Cousineau 002; Florian Faissole; Claude Marché; David Mentré; Hiroaki Inoue (Int. J. Softw. Tools Technol. Transf., 2022)

Slimmer Formal Proofs for Mathematical Libraries. - Paul Geneau de Lamarlière; Guillaume Melquiond; Florian Faissole (ARITH, 2023)

Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function. - Paul Bonnot; Benoît Boyer; Florian Faissole; Claude Marché; Raphaël Rieu-Helft (FMCAD, 2024)

End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. - Florian Faissole; Paul Geneau de Lamarlière; Guillaume Melquiond (ITP, 2024)

Formally-Verified Round-Off Error Analysis of Runge-Kutta Methods. - Florian Faissole (J. Autom. Reason., 2024)