Jean-Christophe Filliâtre

57 papers A* 3A 4B 5C 4Journal 18Unranked 20
YearRankTypeTitle / Venue / Authors
2025 B conf
When Separation Arithmetic is Enough.
iFM
Jean-Christophe Filliâtre, Andrei Paskevich, Olivier Danvy
2025 — conf
coma, an Intermediate Verification Language with Explicit Abstraction Barriers.
ESOP (2)
Andrei Paskevich, Paul Patault, Jean-Christophe Filliâtre
2024 J jnl
Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly.
CoRR
Léo Andrès, Filipe Marques, Arthur Carcano, Pierre Chambart, José Fragoso Santos, Jean-Christophe Filliâtre
2024 J jnl
Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly.
Art Sci. Eng. Program.
Léo Andrès, Filipe Marques, Arthur Carcano, Pierre Chambart, José Fragoso Santos, Jean-Christophe Filliâtre
2022 B conf
Optimizing Prestate Copies in Runtime Verification of Function Postconditions.
RV
Jean-Christophe Filliâtre, Clément Pascutto
2021 B conf
Ortac: Runtime Assertion Checking for OCaml (Tool Paper).
RV
Jean-Christophe Filliâtre, Clément Pascutto
2021 J jnl
Simpler proofs with decentralized invariants.
J. Log. Algebraic Methods Program.
Jean-Christophe Filliâtre
2020 — conf
Abstraction and Genericity in Why3.
ISoLA (1)
Jean-Christophe Filliâtre, Andrei Paskevich
2019 B conf
GOSPEL - Providing OCaml with a Formal Specification Language.
FM
Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira
2016 — conf
A Modular Way to Reason About Iteration.
NFM
Jean-Christophe Filliâtre, Mário Pereira
2016 — conf
Producing All Ideals of a Forest, Formally (Verification Pearl).
VSTTE
Jean-Christophe Filliâtre, Mário Pereira
2016 J jnl
The spirit of ghost code.
Formal Methods Syst. Des.
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
2015 — conf
How to Avoid Proving the Absence of Integer Overflows.
VSTTE
Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich
2015 J jnl
Let's verify this with Why3.
Int. J. Softw. Tools Technol. Transf.
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
2014 J jnl
CAOVerif: An open-source deductive verification platform for cryptographic software implementations.
Sci. Comput. Program.
José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, Bárbara Vieira
2014 — conf
Formalizing Semantics with an Automatic Program Verifier.
VSTTE
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
2014 A* conf
The Spirit of Ghost Code.
CAV
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich
2014 J jnl
Trusting computations: A mechanized proof from partial differential equations to actual program.
Comput. Math. Appl.
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2013 A conf
One Logic to Use Them All.
CADE
Jean-Christophe Filliâtre
2013 — conf
Preserving User Proofs across Specification Changes.
VSTTE
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
2013 J jnl
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program.
J. Autom. Reason.
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2013 A conf
Why3 - Where Programs Meet Provers.
ESOP
Jean-Christophe Filliâtre, Andrei Paskevich
2012 C conf
Discharging Proof Obligations from Atelier B Using Multiple Automated Provers.
ABZ
David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka
2012 C conf
Separation Predicates: A Taste of Separation Logic in First-Order Logic.
ICFEM
François Bobot, Jean-Christophe Filliâtre
2012 — conf
The 2nd Verified Software Competition: Experience Report.
COMPARE
Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump
2012 J jnl
Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program.
CoRR
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2012 — conf
Verifying Two Lines of C with Why3: An Exercise in Program Verification.
VSTTE
Jean-Christophe Filliâtre
2011 — conf
Correct Code Containing Containers.
TAP@TOOLS
Claire Dross, Jean-Christophe Filliâtre, Yannick Moy
2011 J jnl
Deductive software verification.
Int. J. Softw. Tools Technol. Transf.
Jean-Christophe Filliâtre
2011 — conf
Functory: A Distributed Computing Library for Objective Caml.
Trends in Functional Programming
Jean-Christophe Filliâtre, K. Kalyanasundaram
2011 J jnl
Real-Time Monitoring of Ocaml programs.
Stud. Inform. Univ.
Sylvain Conchon, Jean-Christophe Filliâtre, Fabrice Le Fessant, Julien Robert, Guillaume Von Tokarski
2011 — conf
The COST IC0701 Verification Competition 2011.
FoVeOOS
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
2011 J jnl
Wave Equation Numerical Resolution: Mathematics and Program
CoRR
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010 J jnl
A Deductive Verification Platform for Cryptographic Software.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Manuel Barbosa, Jorge Sousa Pinto, Jean-Christophe Filliâtre, Bárbara Vieira
2010 B conf
Formal Proof of a Wave Equation Resolution Scheme: The Method Error.
ITP
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010 J jnl
Formal Proof of a Wave Equation Resolution Scheme: the Method Error
CoRR
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010 — ed.
Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010
PLPV
Jean-Christophe Filliâtre, Cormac Flanagan
2009 — conf
Combining Coq and Gappa for Certifying Floating-Point Programs.
Calculemus/MKM
Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
2009 J jnl
Faire bonne figure avec MLPOST.
Stud. Inform. Univ.
Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, Stéphane Lescuyer
2009 — conf
Faire bonne figure avec Mlpost.
JFLA
Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, Stéphane Lescuyer
2008 — conf
A functional implementation of the garsia--wachs algorithm: (functional pearl).
ML
Jean-Christophe Filliâtre
2008 A conf
Semi-persistent Data Structures.
ESOP
Sylvain Conchon, Jean-Christophe Filliâtre
2007 — conf
A persistent union-find data structure.
ML
Sylvain Conchon, Jean-Christophe Filliâtre
2007 — conf
Designing a Generic Graph Library Using ML Functors.
Trends in Functional Programming
Sylvain Conchon, Jean-Christophe Filliâtre, Julien Signoles
2007 C conf
Formal Verification of Floating-Point Programs.
IEEE Symposium on Computer Arithmetic
Sylvie Boldo, Jean-Christophe Filliâtre
2007 J jnl
Formal proof of a program: Find.
Sci. Comput. Program.
Jean-Christophe Filliâtre
2007 A* conf
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification.
CAV
Jean-Christophe Filliâtre, Claude Marché
2006 — conf
Backtracking iterators.
ML
Jean-Christophe Filliâtre
2006 — conf
Type-safe modular hash-consing.
ML
Jean-Christophe Filliâtre, Sylvain Conchon
2006 — ed.
Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers
TYPES
Jean-Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner
2004 A conf
Functors for Proofs and Programs.
ESOP
Jean-Christophe Filliâtre, Pierre Letouzey
2004 C conf
Multi-prover Verification of C Programs.
ICFEM
Jean-Christophe Filliâtre, Claude Marché
2003 — ed.
Journées francophones des langages applicatifs (JFLA'03), Chamrousse, France, Janvier 2003
JFLA
Jean-Christophe Filliâtre
2003 J jnl
Producing all ideals of a forest, functionally.
J. Funct. Program.
Jean-Christophe Filliâtre, François Pottier
2003 J jnl
Verification of non-functional programs using interpretations in type theory.
J. Funct. Program.
Jean-Christophe Filliâtre
2001 A* conf
ICS: Integrated Canonizer and Solver.
CAV
Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar
1998 — conf
Proof of Imperative Programs in Type Theory.
TYPES
Jean-Christophe Filliâtre