Why3—where programs meet provers JC Filliâtre, A Paskevich Programming Languages and Systems: 22nd European Symposium on Programming …, 2013 | 782 | 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 | 405 | 2011 |
The spirit of ghost code JC Filliâtre, L Gondelman, A Paskevich Formal Methods in System Design 48 (3), 152-174, 2016 | 101 | 2016 |
Let’s verify this with Why3 F Bobot, JC Filliâtre, C Marché, A Paskevich International Journal on Software Tools for Technology Transfer 17 (6), 709-727, 2015 | 85 | 2015 |
TFF1: The TPTP typed first-order form with rank-1 polymorphism JC Blanchette, A Paskevich Automated Deduction–CADE-24: 24th International Conference on Automated …, 2013 | 84 | 2013 |
Expressing polymorphic types in a many-sorted language F Bobot, A Paskevich Frontiers of Combining Systems, 87-102, 2011 | 63 | 2011 |
ForTheL — the language of formal theories K Vershinin, A Paskevich International Journal of Information Theories and Applications 7 (3), 120-126, 2000 | 58 | 2000 |
A3PAT, an approach for certified automated termination proofs É Contejean, A Paskevich, X Urbain, P Courtieu, O Pons, J Forest Proceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and …, 2010 | 48 | 2010 |
System for Automated Deduction (SAD): a tool for proof verification K Verchinine, A Lyaletski, A Paskevich International Conference on Automated Deduction, 398-403, 2007 | 48 | 2007 |
Reasoning with triggers C Dross, S Conchon, A Paskevich | 36 | 2012 |
System for Automated Deduction (SAD): Linguistic and deductive peculiarities A Lyaletski, K Verchinine, A Degtyarev, A Paskevich Intelligent Information Systems 2002: Proceedings of the IIS’2002 Symposium …, 2002 | 33 | 2002 |
Adding Decision Procedures to SMT Solvers using Axioms with Triggers C Dross, S Conchon, J Kanig, A Paskevich Journal of Automated Reasoning 56 (4), 387-457, 2016 | 29 | 2016 |
On correctness of mathematical texts from a logical and practical point of view K Verchinine, A Lyaletski, A Paskevich, A Anisimov Intelligent Computer Mathematics: 9th International Conference, AISC 2008 …, 2008 | 29 | 2008 |
The why3 platform F Bobot, JC Filliâtre, C Marché, G Melquiond, A Paskevich LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, 2011 | 28 | 2011 |
Theorem proving and proof verification in the system SAD A Lyaletski, A Paskevich, K Verchinine International Conference on Mathematical Knowledge Management, 236-250, 2004 | 28 | 2004 |
The 2nd verified software competition: Experience report JC Filliâtre, A Paskevich, A Stump COMPARE 2012, Comparative Empirical Evaluation of Reasoning Systems, 1st …, 2012 | 27 | 2012 |
Preserving user proofs across specification changes F Bobot, JC Filliâtre, C Marché, G Melquiond, A Paskevich Working Conference on Verified Software: Theories, Tools, and Experiments …, 2013 | 26 | 2013 |
A Pragmatic Type System for Deductive Verification JC Filliâtre, L Gondelman, A Paskevich | 24 | 2016 |
VerifyThis 2018: A Program Verification Competition M Huisman, R Monahan, P Müller, A Paskevich, G Ernst Université Paris-Saclay, 2019 | 23 | 2019 |
Formalizing semantics with an automatic program verifier M Clochard, JC Filliâtre, C Marché, A Paskevich Verified Software: Theories, Tools and Experiments: 6th International …, 2014 | 23 | 2014 |