Proof of Imperative Programs in Type Theory. - Jean-Christophe Filliâtre (TYPES, 1998)

ICS: Integrated Canonizer and Solver. - Jean-Christophe Filliâtre; Sam Owre; Harald Rueß; Natarajan Shankar (CAV, 2001)

Verification of non-functional programs using interpretations in type theory. - Jean-Christophe Filliâtre (J. Funct. Program., 2003)

Producing all ideals of a forest, functionally. - Jean-Christophe Filliâtre; François Pottier (J. Funct. Program., 2003)

Functors for Proofs and Programs. - Jean-Christophe Filliâtre; Pierre Letouzey (ESOP, 2004)

Multi-prover Verification of C Programs. - Jean-Christophe Filliâtre; Claude Marché (ICFEM, 2004)

Backtracking iterators. - Jean-Christophe Filliâtre (ML, 2006)

Type-safe modular hash-consing. - Jean-Christophe Filliâtre; Sylvain Conchon (ML, 2006)

Formal Verification of Floating-Point Programs. - Sylvie Boldo; Jean-Christophe Filliâtre (IEEE Symposium on Computer Arithmetic, 2007)

The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. - Jean-Christophe Filliâtre; Claude Marché (CAV, 2007)

A persistent union-find data structure. - Sylvain Conchon; Jean-Christophe Filliâtre (ML, 2007)

Designing a Generic Graph Library Using ML Functors. - Sylvain Conchon; Jean-Christophe Filliâtre; Julien Signoles (Trends in Functional Programming, 2007)

Formal proof of a program: Find. - Jean-Christophe Filliâtre (Sci. Comput. Program., 2007)

Semi-persistent Data Structures. - Sylvain Conchon; Jean-Christophe Filliâtre (ESOP, 2008)

A functional implementation of the garsia–wachs algorithm: (functional pearl). - Jean-Christophe Filliâtre (ML, 2008)

Combining Coq and Gappa for Certifying Floating-Point Programs. - Sylvie Boldo; Jean-Christophe Filliâtre; Guillaume Melquiond (Calculemus/MKM, 2009)

Faire bonne figure avec MLPOST. - Romain Bardou; Jean-Christophe Filliâtre; Johannes Kanig; Stéphane Lescuyer (Stud. Inform. Univ., 2009)

Formal Proof of a Wave Equation Resolution Scheme: The Method Error. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (ITP, 2010)

A Deductive Verification Platform for Cryptographic Software. - Manuel Barbosa; Jorge Sousa Pinto; Jean-Christophe Filliâtre; Bárbara Vieira (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010)

The COST IC0701 Verification Competition 2011. - Thorsten Bormer; Marc Brockschmidt; Dino Distefano; Gidon Ernst; Jean-Christophe Filliâtre; Radu Grigore; Marieke Huisman; Vladimir Klebanov; Claude Marché; Rosemary Monahan; Wojciech Mostowski; Nadia Polikarpova; et al. (FoVeOOS, 2011)

Functory: A Distributed Computing Library for Objective Caml. - Jean-Christophe Filliâtre; K. Kalyanasundaram (Trends in Functional Programming, 2011)

Correct Code Containing Containers. - Claire Dross; Jean-Christophe Filliâtre; Yannick Moy (TAP@TOOLS, 2011)

Wave Equation Numerical Resolution: Mathematics and Program - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (CoRR, 2011)

Real-Time Monitoring of Ocaml programs. - Sylvain Conchon; Jean-Christophe Filliâtre; Fabrice Le Fessant; Julien Robert; Guillaume Von Tokarski (Stud. Inform. Univ., 2011)

Deductive software verification. - Jean-Christophe Filliâtre (Int. J. Softw. Tools Technol. Transf., 2011)

Discharging Proof Obligations from Atelier B Using Multiple Automated Provers. - David Mentré; Claude Marché; Jean-Christophe Filliâtre; Masashi Asuka (ABZ, 2012)

The 2nd Verified Software Competition: Experience Report. - Jean-Christophe Filliâtre; Andrei Paskevich; Aaron Stump (COMPARE, 2012)

Separation Predicates: A Taste of Separation Logic in First-Order Logic. - François Bobot; Jean-Christophe Filliâtre (ICFEM, 2012)

Verifying Two Lines of C with Why3: An Exercise in Program Verification. - Jean-Christophe Filliâtre (VSTTE, 2012)

One Logic to Use Them All. - Jean-Christophe Filliâtre (CADE, 2013)

Why3 - Where Programs Meet Provers. - Jean-Christophe Filliâtre; Andrei Paskevich (ESOP, 2013)

Preserving User Proofs across Specification Changes. - François Bobot; Jean-Christophe Filliâtre; Claude Marché; Guillaume Melquiond; Andrei Paskevich (VSTTE, 2013)

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (J. Autom. Reason., 2013)

Formalizing Semantics with an Automatic Program Verifier. - Martin Clochard; Jean-Christophe Filliâtre; Claude Marché; Andrei Paskevich (VSTTE, 2014)

Trusting computations: A mechanized proof from partial differential equations to actual program. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (Comput. Math. Appl., 2014)

CAOVerif: An open-source deductive verification platform for cryptographic software implementations. - José Bacelar Almeida; Manuel Barbosa; Jean-Christophe Filliâtre; Jorge Sousa Pinto; Bárbara Vieira (Sci. Comput. Program., 2014)

How to Avoid Proving the Absence of Integer Overflows. - Martin Clochard; Jean-Christophe Filliâtre; Andrei Paskevich (VSTTE, 2015)

Let's verify this with Why3. - François Bobot; Jean-Christophe Filliâtre; Claude Marché; Andrei Paskevich (Int. J. Softw. Tools Technol. Transf., 2015)

A Modular Way to Reason About Iteration. - Jean-Christophe Filliâtre; Mário Pereira (NFM, 2016)

Producing All Ideals of a Forest, Formally (Verification Pearl). - Jean-Christophe Filliâtre; Mário Pereira (VSTTE, 2016)

The spirit of ghost code. - Jean-Christophe Filliâtre; Léon Gondelman; Andrei Paskevich (Formal Methods Syst. Des., 2016)

GOSPEL - Providing OCaml with a Formal Specification Language. - Arthur Charguéraud; Jean-Christophe Filliâtre; Cláudio Lourenço; Mário Pereira (FM, 2019)

Abstraction and Genericity in Why3. - Jean-Christophe Filliâtre; Andrei Paskevich (ISoLA (1), 2020)

Ortac: Runtime Assertion Checking for OCaml (Tool Paper). - Jean-Christophe Filliâtre; Clément Pascutto (RV, 2021)

Simpler proofs with decentralized invariants. - Jean-Christophe Filliâtre (J. Log. Algebraic Methods Program., 2021)

Optimizing Prestate Copies in Runtime Verification of Function Postconditions. - Jean-Christophe Filliâtre; Clément Pascutto (RV, 2022)

Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly. - Léo Andrès; Filipe Marques; Arthur Carcano; Pierre Chambart; José Fragoso Santos; Jean-Christophe Filliâtre (Art Sci. Eng. Program., 2024)

coma, an Intermediate Verification Language with Explicit Abstraction Barriers. - Andrei Paskevich; Paul Patault; Jean-Christophe Filliâtre (ESOP (2), 2025)