Follow
Jean-Christophe Filliātre
Jean-Christophe Filliātre
CNRS
Verified email at lri.fr
Title
Cited by
Cited by
Year
Why3—where programs meet provers
JC Filliātre, A Paskevich
Programming Languages and Systems: 22nd European Symposium on Programming …, 2013
6202013
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification: (Tool Paper)
JC Filliātre, C Marché
Computer Aided Verification: 19th International Conference, CAV 2007, Berlin …, 2007
4932007
Why3: Shepherd your herd of provers
F Bobot, JC Filliātre, C Marché, A Paskevich
Boogie 2011: First International Workshop on Intermediate Verification …, 2011
3652011
Multi-prover verification of C programs
JC Filliātre, C Marché
Formal Methods and Software Engineering: 6th International Conference on …, 2004
3002004
The Coq proof assistant reference manual: Version 6.1
B Barras, S Boutin, C Cornes, J Courant, JC Filliatre, E Gimenez, ...
Inria, 1997
2991997
Acsl: Ansi c specification language
P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto
CEA-LIST, Saclay, France, Tech. Rep. v1 2, 2008
2042008
Acsl: Ansi c specification language
P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto
CEA-LIST, Saclay, France, Tech. Rep. v1 2, 2008
2042008
Acsl: Ansi c specification language
P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto
CEA-LIST, Saclay, France, Tech. Rep. v1 2, 2008
2042008
ICS: Integrated Canonizer and Solver?
JC Filliātre, S Owre, H Rue* B, N Shankar
Computer Aided Verification: 13th International Conference, CAV 2001 Paris …, 2001
1832001
Verification of non-functional programs using interpretations in type theory
JC Filliātre
Journal of Functional Programming 13 (4), 709-745, 2003
1492003
Why: a multi-language multi-prover verification tool
JC Filliātre
Research Report 1366, LRI, Université Paris Sud, 2003
1452003
Formal verification of floating-point programs
S Boldo, JC Filliātre
18th IEEE Symposium on Computer Arithmetic (ARITH'07), 187-194, 2007
1242007
Acsl: Ansi
P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto
ISO C specification language 1, 2008
1172008
The Coq proof assistant reference manual
B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ...
INRIA, version 6 (11), 1999
1131999
Combining Coq and Gappa for Certifying Floating-Point Programs.
S Boldo, JC Filliātre, G Melquiond
Calculemus/MKM, 59-74, 2009
972009
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
arXiv preprint arXiv:1112.1795, 2011
932011
Type-safe modular hash-consing
JC Filliātre, S Conchon
Proceedings of the 2006 Workshop on ML, 12-19, 2006
902006
Deductive software verification
JC Filliātre
International Journal on Software Tools for Technology Transfer 13, 397-403, 2011
812011
The spirit of ghost code
JC Filliātre, L Gondelman, A Paskevich
Formal Methods in System Design 48, 152-174, 2016
792016
Functors for proofs and programs
JC Filliātre, P Letouzey
Programming Languages and Systems: 13th European Symposium on Programming …, 2004
702004
The system can't perform the operation now. Try again later.
Articles 1–20