Florian Faissole

According to our database, Florian Faissole authored at least 16 papers between 2017 and 2026.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2026

Verification of Generic VHDL Designs and Their Translation to Rocq.

Ocan Sankur, Benoît Boyer, Florian Faissole

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2026

2024

Formally-Verified Round-Off Error Analysis of Runge-Kutta Methods.

Florian Faissole

J. Autom. Reason., March, 2024

End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation.

Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function.

Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft

Proceedings of the Formal Methods in Computer-Aided Design, 2024

2023

Slimmer Formal Proofs for Mathematical Libraries.

Paul Geneau de Lamarlière, Guillaume Melquiond, Florian Faissole

Proceedings of the 30th IEEE Symposium on Computer Arithmetic, 2023

2022

Automated formal analysis of temporal properties of Ladder programs.

Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue

Int. J. Softw. Tools Technol. Transf., 2022

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

2021

Synthetic topology in Homotopy Type Theory for probabilistic programming.

Martin E. Bidlingmaier, Florian Faissole, Bas Spitters

Math. Struct. Comput. Sci., 2021

Automated Verification of Temporal Properties of Ladder Programs.

Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue

Proceedings of the Formal Methods for Industrial Critical Systems, 2021

2020

Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods.

Sylvie Boldo, Florian Faissole, Alexandre Chapoutot

IEEE Trans. Computers, 2020

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

PhD thesis, 2019

Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis.

Florian Faissole, George A. Constantinides, David B. Thomas

Proceedings of the 27th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2019

2018

A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers.

Sylvie Boldo, Florian Faissole, Vincent Tourneur

Proceedings of the 25th IEEE Symposium on Computer Arithmetic, 2018

2017

Formalization and Closedness of Finite Dimensional Subspaces.

Florian Faissole

Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

A Coq formal proof of the LaxMilgram theorem.

Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

Round-off Error Analysis of Explicit One-Step Numerical Integration Methods.

Sylvie Boldo, Florian Faissole, Alexandre Chapoutot

Proceedings of the 24th IEEE Symposium on Computer Arithmetic, 2017