Andrei Paskevich
Andrei Paskevich
Associate Professor of Computer Science, Paris-Saclay University
Verified email at - Homepage
Cited by
Cited by
Why3—where programs meet provers
JC Filliâtre, A Paskevich
Programming Languages and Systems: 22nd European Symposium on Programming …, 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
The spirit of ghost code
JC Filliâtre, L Gondelman, A Paskevich
Formal Methods in System Design 48 (3), 152-174, 2016
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
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
Expressing polymorphic types in a many-sorted language
F Bobot, A Paskevich
Frontiers of Combining Systems, 87-102, 2011
ForTheL — the language of formal theories
K Vershinin, A Paskevich
International Journal of Information Theories and Applications 7 (3), 120-126, 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
System for Automated Deduction (SAD): a tool for proof verification
K Verchinine, A Lyaletski, A Paskevich
International Conference on Automated Deduction, 398-403, 2007
Reasoning with triggers
C Dross, S Conchon, A Paskevich
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
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
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
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
Theorem proving and proof verification in the system SAD
A Lyaletski, A Paskevich, K Verchinine
International Conference on Mathematical Knowledge Management, 236-250, 2004
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
The 2nd verified software competition: Experience report
JC Filliâtre, A Paskevich, A Stump
COMPARE 2012, Comparative Empirical Evaluation of Reasoning Systems, 1st …, 2012
A Pragmatic Type System for Deductive Verification
JC Filliâtre, L Gondelman, A Paskevich
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
VerifyThis 2018: A Program Verification Competition
M Huisman, R Monahan, P Müller, A Paskevich, G Ernst
Université Paris-Saclay, 2019
The system can't perform the operation now. Try again later.
Articles 1–20