| The Why/Krakatoa/Caduceus platform for deductive program verification JC Filliâtre, C Marché International Conference on Computer Aided Verification, 173-177, 2007 | 464 | 2007 |
| Why3—where programs meet provers JC Filliâtre, A Paskevich European symposium on programming, 125-128, 2013 | 452 | 2013 |
| Why3: Shepherd your herd of provers F Bobot, JC Filliâtre, C Marché, A Paskevich Boogie 2011: First International Workshop on Intermediate Verification …, 2011 | 314 | 2011 |
| Multi-prover verification of C programs JC Filliâtre, C Marché International Conference on Formal Engineering Methods, 15-29, 2004 | 282 | 2004 |
| The Coq proof assistant reference manual: Version 6.1 B Barras, S Boutin, C Cornes, J Courant, JC Filliatre, E Gimenez, ... Inria, 1997 | 262 | 1997 |
| ICS: Integrated Canonizer and Solver? JC Filliâtre, S Owre, H Rue, N Shankar International Conference on Computer Aided Verification, 246-249, 2001 | 182 | 2001 |
| 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 | 180 | 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 | 180 | 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 | 180 | 2008 |
| Why: a multi-language multi-prover verification tool JC Filliâtre | 142 | 2003 |
| Verification of non-functional programs using interpretations in type theory JC Filliâtre Journal of Functional Programming 13 (4), 709, 2003 | 140 | 2003 |
| Formal verification of floating-point programs S Boldo, JC Filliâtre 18th IEEE Symposium on Computer Arithmetic (ARITH'07), 187-194, 2007 | 120 | 2007 |
| Acsl: Ansi P Baudin, JC Filliâtre, C Marché, B Monate, Y Moy, V Prevosto ISO C specification language, 2008 | 104 | 2008 |
| The Coq proof assistant reference manual B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ... INRIA, version 6 (11), 1999 | 90 | 1999 |
| 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 | 81 | 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 Journal of Automated Reasoning 50 (4), 423-456, 2013 | 75 | 2013 |
| Type-safe modular hash-consing JC Filliâtre, S Conchon Proceedings of the 2006 Workshop on ML, 12-19, 2006 | 70 | 2006 |
| The spirit of ghost code JC Filliâtre, L Gondelman, A Paskevich Formal Methods in System Design 48 (3), 152-174, 2016 | 62 | 2016 |
| Functors for proofs and programs JC Filliâtre, P Letouzey European Symposium on Programming, 370-384, 2004 | 61 | 2004 |
| The Coq proof assistant reference manual C Cornes, J Courant, JC Filliâtre, G Huet, P Manoury, C Paulin-Mohring, ... Rapport Technique 177, 1995 | 61 | 1995 |
Claude MarchéSenior Research Scientist, InriaBestätigte E-Mail-Adresse bei inria.fr
