| 2026 | FORTE | Sound Automatic Lock Placement for Concurrent Programs with Pointers. | Nicolas Waldburger, Florian Faissole, Ryo Okabe, Denis Cousineau |
| 2026 | VMCAI | Verification of Generic VHDL Designs and Their Translation to Rocq. | Ocan Sankur, Benot Boyer, Florian Faissole |
| 2024 | FMCAD | Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function. | Paul Bonnot, Benot Boyer, Florian Faissole, Claude March, Raphal Rieu-Helft |
| 2024 | ITP | End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. | Florian Faissole, Paul Geneau de Lamarlire, Guillaume Melquiond |
| 2023 | ARITH | Slimmer Formal Proofs for Mathematical Libraries. | Paul Geneau de Lamarlire, Guillaume Melquiond, Florian Faissole |
| 2021 | FMICS | Automated Verification of Temporal Properties of Ladder Programs. | Cludio Belo Loureno, Denis Cousineau, Florian Faissole, Claude March, David Mentr, Hiroaki Inoue |
| 2019 | FCCM | Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis. | Florian Faissole, George A. Constantinides, David B. Thomas |
| 2018 | ARITH | A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. | Sylvie Boldo, Florian Faissole, Vincent Tourneur |
| 2017 | ARITH | Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. | Sylvie Boldo, Florian Faissole, Alexandre Chapoutot |
| 2017 | CPP | A Coq formal proof of the LaxMilgram theorem. | Sylvie Boldo, Franois Clment, Florian Faissole, Vincent Martin, Micaela Mayero |
| 2017 | SYNASC | Formalization and Closedness of Finite Dimensional Subspaces. | Florian Faissole |