| Why3—where programs meet provers JC Filliātre, A Paskevich Programming Languages and Systems: 22nd European Symposium on Programming …, 2013 | 622 | 2013 |
| 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 | 493 | 2007 |
| Why3: Shepherd your herd of provers F Bobot, JC Filliātre, C Marché, A Paskevich Boogie 2011: First International Workshop on Intermediate Verification …, 2011 | 365 | 2011 |
| The Coq proof assistant reference manual: Version 6.1 B Barras, S Boutin, C Cornes, J Courant, JC Filliatre, E Gimenez, ... Inria, 1997 | 301 | 1997 |
| Multi-prover verification of C programs JC Filliātre, C Marché Formal Methods and Software Engineering: 6th International Conference on …, 2004 | 300 | 2004 |
| 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 | 204 | 2008 |
| 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 | 204 | 2008 |
| 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 | 204 | 2008 |
| 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 | 183 | 2001 |
| Verification of non-functional programs using interpretations in type theory JC Filliātre Journal of Functional Programming 13 (4), 709-745, 2003 | 149 | 2003 |
| Why: a multi-language multi-prover verification tool JC Filliātre Research Report 1366, LRI, Université Paris Sud, 2003 | 145 | 2003 |
| Formal verification of floating-point programs S Boldo, JC Filliātre 18th IEEE Symposium on Computer Arithmetic (ARITH'07), 187-194, 2007 | 124 | 2007 |
| Acsl: Ansi P Baudin, JC Filliātre, C Marché, B Monate, Y Moy, V Prevosto ISO C specification language 1, 2008 | 117 | 2008 |
| The Coq proof assistant reference manual B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ... INRIA, version 6 (11), 1999 | 113 | 1999 |
| Combining Coq and Gappa for Certifying Floating-Point Programs. S Boldo, JC Filliātre, G Melquiond Calculemus/MKM, 59-74, 2009 | 97 | 2009 |
| 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 | 93 | 2011 |
| Type-safe modular hash-consing JC Filliātre, S Conchon Proceedings of the 2006 Workshop on ML, 12-19, 2006 | 90 | 2006 |
| Deductive software verification JC Filliātre International Journal on Software Tools for Technology Transfer 13, 397-403, 2011 | 81 | 2011 |
| The spirit of ghost code JC Filliātre, L Gondelman, A Paskevich Formal Methods in System Design 48, 152-174, 2016 | 79 | 2016 |
| Functors for proofs and programs JC Filliātre, P Letouzey Programming Languages and Systems: 13th European Symposium on Programming …, 2004 | 71 | 2004 |
Claude MarchéSenior Research Scientist, InriaGeverifieerd e-mailadres voor inria.fr
