Florian Faissole

18 papers B 4C 4Misc 2Journal 7
YearRankTypeTitle / Venue / Authors
2026 B conf
Verification of Generic VHDL Designs and Their Translation to Rocq.
VMCAI
Ocan Sankur, Benoît Boyer, Florian Faissole
2024 B conf
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation.
ITP
Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond
2024 B conf
Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function.
FMCAD
Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft
2024 J jnl
Formally-Verified Round-Off Error Analysis of Runge-Kutta Methods.
J. Autom. Reason.
Florian Faissole
2023 C conf
Slimmer Formal Proofs for Mathematical Libraries.
ARITH
Paul Geneau de Lamarlière, Guillaume Melquiond, Florian Faissole
2022 J jnl
A Coq Formalization of Lebesgue Integration of Nonnegative Functions.
J. Autom. Reason.
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2022 J jnl
Automated formal analysis of temporal properties of Ladder programs.
Int. J. Softw. Tools Technol. Transf.
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
2021 J jnl
A Coq Formalization of Lebesgue Integration of Nonnegative Functions.
CoRR
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2021 C conf
Automated Verification of Temporal Properties of Ladder Programs.
FMICS
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
2021 J jnl
Synthetic topology in Homotopy Type Theory for probabilistic programming.
Math. Struct. Comput. Sci.
Martin E. Bidlingmaier, Florian Faissole, Bas Spitters
2020 J jnl
Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods.
IEEE Trans. Computers
Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
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 Misc conf
Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis.
FCCM
Florian Faissole, George A. Constantinides, David B. Thomas
2019 J jnl
Synthetic topology in Homotopy Type Theory for probabilistic programming.
CoRR
Martin E. Bidlingmaier, Florian Faissole, Bas Spitters
2018 C conf
A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers.
ARITH
Sylvie Boldo, Florian Faissole, Vincent Tourneur
2017 B conf
A Coq formal proof of the LaxMilgram theorem.
CPP
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2017 Misc conf
Formalization and Closedness of Finite Dimensional Subspaces.
SYNASC
Florian Faissole
2017 C conf
Round-off Error Analysis of Explicit One-Step Numerical Integration Methods.
ARITH
Sylvie Boldo, Florian Faissole, Alexandre Chapoutot