Jean-Christophe Filliâtre

According to our database, Jean-Christophe Filliâtre authored at least 47 papers between 1998 and 2024.

Collaborative distances:

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

2024

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

CoRR, 2024

2022

Optimizing Prestate Copies in Runtime Verification of Function Postconditions.

Jean-Christophe Filliâtre, Clément Pascutto

Proceedings of the Runtime Verification - 22nd International Conference, 2022

2021

Simpler proofs with decentralized invariants.

Jean-Christophe Filliâtre

J. Log. Algebraic Methods Program., 2021

Ortac: Runtime Assertion Checking for OCaml (Tool Paper).

Jean-Christophe Filliâtre, Clément Pascutto

Proceedings of the Runtime Verification - 21st International Conference, 2021

2020

Abstraction and Genericity in Why3.

Jean-Christophe Filliâtre, Andrei Paskevich

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

2019

GOSPEL - Providing OCaml with a Formal Specification Language.

Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2016

The spirit of ghost code.

Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich

Formal Methods Syst. Des., 2016

Producing All Ideals of a Forest, Formally (Verification Pearl).

Jean-Christophe Filliâtre, Mário Pereira

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2016

A Modular Way to Reason About Iteration.

Jean-Christophe Filliâtre, Mário Pereira

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

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

How to Avoid Proving the Absence of Integer Overflows.

Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich

Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

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

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

Formalizing Semantics with an Automatic Program Verifier.

Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

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

Preserving User Proofs across Specification Changes.

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Why3 - Where Programs Meet Provers.

Jean-Christophe Filliâtre, Andrei Paskevich

Proceedings of the Programming Languages and Systems, 2013

One Logic to Use Them All.

Jean-Christophe Filliâtre

Proceedings of the Automated Deduction - CADE-24, 2013

2012

Verifying Two Lines of C with Why3: An Exercise in Program Verification.

Jean-Christophe Filliâtre

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Separation Predicates: A Taste of Separation Logic in First-Order Logic.

François Bobot, Jean-Christophe Filliâtre

Proceedings of the Formal Methods and Software Engineering, 2012

The 2nd Verified Software Competition: Experience Report.

Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump

Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

Discharging Proof Obligations from Atelier B Using Multiple Automated Provers.

David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

2011

Deductive software verification.

Jean-Christophe Filliâtre

Int. J. Softw. Tools Technol. Transf., 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

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

Correct Code Containing Containers.

Claire Dross, Jean-Christophe Filliâtre, Yannick Moy

Proceedings of the Tests and Proofs - 5th International Conference, 2011

Functory: A Distributed Computing Library for Objective Caml.

Jean-Christophe Filliâtre, K. Kalyanasundaram

Proceedings of the Trends in Functional Programming, 12th International Symposium, 2011

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, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, Mattias Ulbrich

Proceedings of the Formal Verification of Object-Oriented Software, 2011

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

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

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Faire bonne figure avec MLPOST.

Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, Stéphane Lescuyer

Stud. Inform. Univ., 2009

Combining Coq and Gappa for Certifying Floating-Point Programs.

Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond

Proceedings of the Intelligent Computer Mathematics, 2009

2008

A functional implementation of the garsia--wachs algorithm: (functional pearl).

Jean-Christophe Filliâtre

Proceedings of the ACM Workshop on ML, 2008, Victoria, BC, Canada, September 21, 2008, 2008

Semi-persistent Data Structures.

Sylvain Conchon, Jean-Christophe Filliâtre

Proceedings of the Programming Languages and Systems, 2008

2007

Formal proof of a program: Find.

Jean-Christophe Filliâtre

Sci. Comput. Program., 2007

Designing a Generic Graph Library Using ML Functors.

Sylvain Conchon, Jean-Christophe Filliâtre, Julien Signoles

Proceedings of the Eighth Symposium on Trends in Functional Programming, 2007

A persistent union-find data structure.

Sylvain Conchon, Jean-Christophe Filliâtre

Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, October 5, 2007, 2007

The Why/Krakatoa/Caduceus Platform for Deductive Program Verification.

Jean-Christophe Filliâtre, Claude Marché

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Formal Verification of Floating-Point Programs.

Sylvie Boldo, Jean-Christophe Filliâtre

Proceedings of the 18th IEEE Symposium on Computer Arithmetic (ARITH-18 2007), 2007

2006

Type-safe modular hash-consing.

Jean-Christophe Filliâtre, Sylvain Conchon

Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, 2006

Backtracking iterators.

Jean-Christophe Filliâtre

Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, 2006

2004

Multi-prover Verification of C Programs.

Jean-Christophe Filliâtre, Claude Marché

Proceedings of the Formal Methods and Software Engineering, 2004

Functors for Proofs and Programs.

Jean-Christophe Filliâtre, Pierre Letouzey

Proceedings of the Programming Languages and Systems, 2004

2003

Producing all ideals of a forest, functionally.

Jean-Christophe Filliâtre, François Pottier

J. Funct. Program., 2003

Verification of non-functional programs using interpretations in type theory.

Jean-Christophe Filliâtre

J. Funct. Program., 2003

2001

ICS: Integrated Canonizer and Solver.

Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

1998

Proof of Imperative Programs in Type Theory.

Jean-Christophe Filliâtre

Proceedings of the Types for Proofs and Programs, 1998