default search action
Jean-Christophe Filliâtre
Person information
- affiliation: University of Paris-Sud, Laboratory for Computer Science
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2022
- [c34]Jean-Christophe Filliâtre, Clément Pascutto
:
Optimizing Prestate Copies in Runtime Verification of Function Postconditions. RV 2022: 85-104 - 2021
- [j13]Jean-Christophe Filliâtre:
Simpler proofs with decentralized invariants. J. Log. Algebraic Methods Program. 121: 100645 (2021) - [c33]Jean-Christophe Filliâtre, Clément Pascutto
Ortac: Runtime Assertion Checking for OCaml (Tool Paper). RV 2021: 244-253 - 2020
- [c32]Jean-Christophe Filliâtre, Andrei Paskevich:
Abstraction and Genericity in Why3. ISoLA (1) 2020: 122-142
2010 – 2019
- 2019
- [c31]Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço
GOSPEL - Providing OCaml with a Formal Specification Language. FM 2019: 484-501 - 2016
- [j12]Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich:
The spirit of ghost code. Formal Methods Syst. Des. 48(3): 152-174 (2016) - [c30]Jean-Christophe Filliâtre, Mário Pereira
A Modular Way to Reason About Iteration. NFM 2016: 322-336 - [c29]Jean-Christophe Filliâtre, Mário Pereira
Producing All Ideals of a Forest, Formally (Verification Pearl). VSTTE 2016: 46-55 - 2015
- [j11]François Bobot
Let's verify this with Why3. Int. J. Softw. Tools Technol. Transf. 17(6): 709-727 (2015) - [c28]Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich:
How to Avoid Proving the Absence of Integer Overflows. VSTTE 2015: 94-109 - 2014
- [j10]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond
Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68(3): 325-352 (2014) - [j9]José Bacelar Almeida
CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Sci. Comput. Program. 91: 216-233 (2014) - [c27]Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich:
The Spirit of Ghost Code. CAV 2014: 1-16 - [c26]Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich:
Formalizing Semantics with an Automatic Program Verifier. VSTTE 2014: 37-51 - 2013
- [j8]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. 50(4): 423-456 (2013) - [c25]Jean-Christophe Filliâtre:
One Logic to Use Them All. CADE 2013: 1-20 - [c24]Jean-Christophe Filliâtre, Andrei Paskevich:
Why3 - Where Programs Meet Provers. ESOP 2013: 125-128 - [c23]François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich:
Preserving User Proofs across Specification Changes. VSTTE 2013: 191-201 - 2012
- [c22]David Mentré, Claude Marché, Jean-Christophe Filliâtre, Masashi Asuka:
Discharging Proof Obligations from Atelier B Using Multiple Automated Provers. ABZ 2012: 238-251 - [c21]Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump:
The 2nd Verified Software Competition: Experience Report. COMPARE 2012: 36-49 - [c20]François Bobot
Separation Predicates: A Taste of Separation Logic in First-Order Logic. ICFEM 2012: 167-181 - [c19]Jean-Christophe Filliâtre:
Verifying Two Lines of C with Why3: An Exercise in Program Verification. VSTTE 2012: 83-97 - [i3]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 abs/1212.6641 (2012) - 2011
- [j7]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) - [j6]Jean-Christophe Filliâtre:
Deductive software verification. Int. J. Softw. Tools Technol. Transf. 13(5): 397-403 (2011) - [c18]Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst
The COST IC0701 Verification Competition 2011. FoVeOOS 2011: 3-21 - [c17]Jean-Christophe Filliâtre, K. Kalyanasundaram:
Functory: A Distributed Computing Library for Objective Caml. Trends in Functional Programming 2011: 65-81 - [c16]Claire Dross, Jean-Christophe Filliâtre, Yannick Moy:
Correct Code Containing Containers. TAP@TOOLS 2011: 102-118 - [i2]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) - 2010
- [j5]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) - [c15]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP 2010: 147-162 - [e3]Jean-Christophe Filliâtre, Cormac Flanagan:
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 [contents] - [i1]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)
2000 – 2009
- 2009
- [j4]Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, Stéphane Lescuyer:
Faire bonne figure avec MLPOST. Stud. Inform. Univ. 7(2): 225-252 (2009) - [c14]Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, Stéphane Lescuyer:
Faire bonne figure avec Mlpost. JFLA 2009: 477-507 - [c13]Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus/MKM 2009: 59-74 - 2008
- [c12]Sylvain Conchon, Jean-Christophe Filliâtre:
Semi-persistent Data Structures. ESOP 2008: 322-336 - [c11]Jean-Christophe Filliâtre:
A functional implementation of the garsia--wachs algorithm: (functional pearl). ML 2008: 91-96 - 2007
- [j3]Jean-Christophe Filliâtre:
Formal proof of a program: Find. Sci. Comput. Program. 64(3): 332-340 (2007) - [c10]Sylvie Boldo, Jean-Christophe Filliâtre:
Formal Verification of Floating-Point Programs. IEEE Symposium on Computer Arithmetic 2007: 187-194 - [c9]Jean-Christophe Filliâtre, Claude Marché:
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. CAV 2007: 173-177 - [c8]Sylvain Conchon, Jean-Christophe Filliâtre:
A persistent union-find data structure. ML 2007: 37-46 - [c7]Sylvain Conchon, Jean-Christophe Filliâtre, Julien Signoles:
Designing a Generic Graph Library Using ML Functors. Trends in Functional Programming 2007: 124-140 - 2006
- [c6]Jean-Christophe Filliâtre, Sylvain Conchon:
Type-safe modular hash-consing. ML 2006: 12-19 - [c5]Jean-Christophe Filliâtre:
Backtracking iterators. ML 2006: 55-62 - [e2]Jean-Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner:
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 [contents] - 2004
- [c4]Jean-Christophe Filliâtre, Pierre Letouzey:
Functors for Proofs and Programs. ESOP 2004: 370-384 - [c3]Jean-Christophe Filliâtre, Claude Marché:
Multi-prover Verification of C Programs. ICFEM 2004: 15-29 - 2003
- [j2]Jean-Christophe Filliâtre:
Verification of non-functional programs using interpretations in type theory. J. Funct. Program. 13(4): 709-745 (2003) - [j1]Jean-Christophe Filliâtre, François Pottier:
Producing all ideals of a forest, functionally. J. Funct. Program. 13(5): 945-956 (2003) - [e1]Jean-Christophe Filliâtre:
Journées francophones des langages applicatifs (JFLA'03), Chamrousse, France, Janvier 2003. Collection Didactique, INRIA 2003 [contents] - 2001
- [c2]Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar:
ICS: Integrated Canonizer and Solver. CAV 2001: 246-249
1990 – 1999
- 1998
- [c1]Jean-Christophe Filliâtre:
Proof of Imperative Programs in Type Theory. TYPES 1998: 78-92
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-08 21:43 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: