Jean-Christophe Filliâtre

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. Reasoning 50(4): 423-456 (2013)

Jean-Christophe Filliâtre, Andrei Paskevich: Why3 - Where Programs Meet Provers. ESOP 2013: 125-128

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

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

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

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

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): 159-185 (2011)

Jean-Christophe Filliâtre: Deductive software verification. STTT 13(5): 397-403 (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: 3-21

Claire Dross, Jean-Christophe Filliâtre, Yannick Moy: Correct Code Containing Containers. TAP 2011: 102-118

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

Manuel Barbosa, Jorge Sousa Pinto, Jean-Christophe Filliâtre, Bárbara Vieira: A Deductive Verification Platform for Cryptographic Software. ECEASST 33 (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: 147-162

Jean-Christophe Filliâtre, Cormac Flanagan (Eds.): Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010. ACM 2010, isbn 978-1-60558-890-2

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 abs/1001.4898 (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. CoRR abs/1005.0824 (2010)

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

Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, Stéphane Lescuyer: Faire bonne figure avec Mlpost. JFLA 2009: 477-507

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

Sylvain Conchon, Jean-Christophe Filliâtre: Semi-persistent Data Structures. ESOP 2008: 322-336

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

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

Sylvie Boldo, Jean-Christophe Filliâtre: Formal Verification of Floating-Point Programs. IEEE Symposium on Computer Arithmetic 2007: 187-194

Jean-Christophe Filliâtre, Claude Marché: The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. CAV 2007: 173-177

Sylvain Conchon, Jean-Christophe Filliâtre: A persistent union-find data structure. ML 2007: 37-46

Jean-Christophe Filliâtre, Sylvain Conchon: Type-safe modular hash-consing. ML 2006: 12-19

Jean-Christophe Filliâtre: Backtracking iterators. ML 2006: 55-62

Jean-Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner (Eds.): Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3839, Springer 2006, isbn 3-540-31428-8

Jean-Christophe Filliâtre, Pierre Letouzey: Functors for Proofs and Programs. ESOP 2004: 370-384

Jean-Christophe Filliâtre, Claude Marché: Multi-prover Verification of C Programs. ICFEM 2004: 15-29

Jean-Christophe Filliâtre: Verification of non-functional programs using interpretations in type theory. J. Funct. Program. 13(4): 709-745 (2003)

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

Jean-Christophe Filliâtre (Ed.): Journées francophones des langages applicatifs (JFLA'03), Chamrousse, France, Janvier 2003. Collection Didactique, INRIA 2003

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

Jean-Christophe Filliâtre: Proof of Imperative Programs in Type Theory. TYPES 1998: 78-92