Jean-Christophe Filliātre
Jean-Christophe Filliātre
CNRS
Verified email at lri.fr
Title
Cited by
Cited by
Year
The Why/Krakatoa/Caduceus platform for deductive program verification
JC Filliātre, C Marché
International Conference on Computer Aided Verification, 173-177, 2007
4642007
Why3—where programs meet provers
JC Filliātre, A Paskevich
European symposium on programming, 125-128, 2013
4412013
Why3: Shepherd your herd of provers
F Bobot, JC Filliātre, C Marché, A Paskevich
3142011
Multi-prover verification of C programs
JC Filliātre, C Marché
International Conference on Formal Engineering Methods, 15-29, 2004
2812004
The Coq proof assistant reference manual: Version 6.1
B Barras, S Boutin, C Cornes, J Courant, JC Filliatre, E Gimenez, ...
2631997
ICS: Integrated Canonizer and Solver?
JC Filliātre, S Owre, H Rue, N Shankar
International Conference on Computer Aided Verification, 246-249, 2001
1862001
Acsl: Ansi c specification language
P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto
Octobre, 2008
1712008
Acsl: Ansi c specification language
P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto
Octobre, 2008
1712008
Acsl: Ansi c specification language
P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto
Octobre, 2008
1712008
Why: a multi-language multi-prover verification tool
JC Filliātre
1442003
Verification of non-functional programs using interpretations in type theory
JC Filliātre
Journal of Functional Programming 13 (4), 709-745, 2003
1402003
Formal verification of floating-point programs
S Boldo, JC Filliātre
18th IEEE Symposium on Computer Arithmetic (ARITH'07), 187-194, 2007
1202007
Acsl: Ansi
P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto
ISO C specification language, 2008
1062008
The Coq proof assistant reference manual
B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ...
INRIA, version 6 (11), 1999
911999
Combining Coq and Gappa for certifying floating-point programs
S Boldo, JC Filliātre, G Melquiond
International Conference on Intelligent Computer Mathematics, 59-74, 2009
762009
Type-safe modular hash-consing
JC Filliātre, S Conchon
Proceedings of the 2006 workshop on ML, 12-19, 2006
742006
Wave equation numerical resolution: a comprehensive mechanized proof of a C program
S Boldo, F Clément, JC Filliātre, M Mayero, G Melquiond, P Weis
Journal of Automated Reasoning 50 (4), 423-456, 2013
722013
The spirit of ghost code
JC Filliātre, L Gondelman, A Paskevich
Formal Methods in System Design 48 (3), 152-174, 2016
612016
Functors for proofs and programs
JC Filliātre, P Letouzey
European Symposium on Programming, 370-384, 2004
602004
The Coq proof assistant reference manual
C Cornes, J Courant, JC Filliātre, G Huet, P Manoury, C Paulin-Mohring, ...
Rapport Technique 177, 1995
591995
The system can't perform the operation now. Try again later.
Articles 1–20