Jean-Christophe Filliâtre

Publication Activity (10 Years)

Years Active: 1998-2022
Publications (10 Years): 8

Top Topics

Ambrosio Tortorelli

Software Implementation

Partial Differential Equations

Top Venues

J. Log. Algebraic Methods Program.

Int. J. Softw. Tools Technol. Transf.

Publications

Jean-Christophe Filliâtre, Clément Pascutto
Optimizing Prestate Copies in Runtime Verification of Function Postconditions. RV (2022)
Jean-Christophe Filliâtre, Clément Pascutto
Ortac: Runtime Assertion Checking for OCaml (Tool Paper). RV (2021)
Jean-Christophe Filliâtre
Simpler proofs with decentralized invariants. J. Log. Algebraic Methods Program. 121 (2021)
Jean-Christophe Filliâtre, Andrei Paskevich
Abstraction and Genericity in Why3. ISoLA (1) (2020)
Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira
GOSPEL - Providing OCaml with a Formal Specification Language. FM (2019)
Jean-Christophe Filliâtre, Mário Pereira
A Modular Way to Reason About Iteration. NFM (2016)
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
The spirit of ghost code. Formal Methods Syst. Des. 48 (3) (2016)
Jean-Christophe Filliâtre, Mário Pereira
Producing All Ideals of a Forest, Formally (Verification Pearl). VSTTE (2016)
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
Let's verify this with Why3. Int. J. Softw. Tools Technol. Transf. 17 (6) (2015)
Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich
How to Avoid Proving the Absence of Integer Overflows. VSTTE (2015)
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
Formalizing Semantics with an Automatic Program Verifier. VSTTE (2014)
José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, Bárbara Vieira
CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Sci. Comput. Program. 91 (2014)
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
The Spirit of Ghost Code. CAV (2014)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68 (3) (2014)
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
Preserving User Proofs across Specification Changes. VSTTE (2013)
Jean-Christophe Filliâtre
One Logic to Use Them All. CADE (2013)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. 50 (4) (2013)
Jean-Christophe Filliâtre, Andrei Paskevich
Why3 - Where Programs Meet Provers. ESOP (2013)
Jean-Christophe Filliâtre
Verifying Two Lines of C with Why3: An Exercise in Program Verification. VSTTE (2012)
David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka
Discharging Proof Obligations from Atelier B Using Multiple Automated Provers. ABZ (2012)
Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump
The 2nd Verified Software Competition: Experience Report. COMPARE (2012)
François Bobot, Jean-Christophe Filliâtre
Separation Predicates: A Taste of Separation Logic in First-Order Logic. ICFEM (2012)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. CoRR (2012)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Wave Equation Numerical Resolution: Mathematics and Program CoRR (2011)
Jean-Christophe Filliâtre
Deductive software verification. Int. J. Softw. Tools Technol. Transf. 13 (5) (2011)
Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, Guillaume Von Tokarski
Real-Time Monitoring of Ocaml programs. Stud. Inform. Univ. 9 (1) (2011)
Jean-Christophe Filliâtre, K. Kalyanasundaram
Functory: A Distributed Computing Library for Objective Caml. Trends in Functional Programming (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, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, Mattias Ulbrich
The COST IC0701 Verification Competition 2011. FoVeOOS (2011)
Claire Dross, Jean-Christophe Filliâtre, Yannick Moy
Correct Code Containing Containers. TAP@TOOLS (2011)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Formal Proof of a Wave Equation Resolution Scheme: the Method Error CoRR (2010)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP (2010)
Manuel Barbosa, Jorge Sousa Pinto, Jean-Christophe Filliâtre, Bárbara Vieira
A Deductive Verification Platform for Cryptographic Software. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 33 (2010)
Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, Stéphane Lescuyer
Faire bonne figure avec Mlpost. JFLA (2009)
Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, Stéphane Lescuyer
Faire bonne figure avec MLPOST. Stud. Inform. Univ. 7 (2) (2009)
Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus/MKM (2009)
Sylvain Conchon, Jean-Christophe Filliâtre
Semi-persistent Data Structures. ESOP (2008)
Jean-Christophe Filliâtre
A functional implementation of the garsia--wachs algorithm: (functional pearl). ML (2008)
Jean-Christophe Filliâtre
Formal proof of a program: Find. Sci. Comput. Program. 64 (3) (2007)
Sylvain Conchon, Jean-Christophe Filliâtre, Julien Signoles
Designing a Generic Graph Library Using ML Functors. Trends in Functional Programming (2007)
Sylvie Boldo, Jean-Christophe Filliâtre
Formal Verification of Floating-Point Programs. IEEE Symposium on Computer Arithmetic (2007)
Jean-Christophe Filliâtre, Claude Marché
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. CAV (2007)
Sylvain Conchon, Jean-Christophe Filliâtre
A persistent union-find data structure. ML (2007)
Jean-Christophe Filliâtre, Sylvain Conchon
Type-safe modular hash-consing. ML (2006)
Jean-Christophe Filliâtre
Backtracking iterators. ML (2006)
Jean-Christophe Filliâtre, Pierre Letouzey
Functors for Proofs and Programs. ESOP (2004)
Jean-Christophe Filliâtre, Claude Marché
Multi-prover Verification of C Programs. ICFEM (2004)
Jean-Christophe Filliâtre, François Pottier
Producing all ideals of a forest, functionally. J. Funct. Program. 13 (5) (2003)
Jean-Christophe Filliâtre
Verification of non-functional programs using interpretations in type theory. J. Funct. Program. 13 (4) (2003)
Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar
ICS: Integrated Canonizer and Solver. CAV (2001)
Jean-Christophe Filliâtre
Proof of Imperative Programs in Type Theory. TYPES (1998)