 |
 |
 |
 |
|
|
||
|---|---|---|
|
hal-00825086v1
Communication dans un congrès
Jasmin Blanchette, Andrei Paskevich. TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism M.P. Bonacina. CADE - 24th International Conference on Automated Deduction - 2013, Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.414-420, 2013, LNCS |
||
|
inria-00535655v1
Communication dans un congrès
Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons et al. A3PAT, an Approach for Certified Automated Termination Proofs John Gallagher and Janis Voigtländer. 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Jan 2010, Madrid, Spain. ACM, pp.63-72, 2010, PEPM'10. <10.1145/1706356.1706370> |
||
|
hal-00915931v1
Pré-publication, Document de travail
Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich. Adding Decision Procedures to SMT Solvers using Axioms with Triggers 2013 |
||
|
hal-01067197v1
Communication dans un congrès
Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Formalizing Semantics with an Automatic Program Verifier Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science |
||
|
hal-01256434v3
Pré-publication, Document de travail
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. A Pragmatic Type System for Deductive Verification 2016 |
||
|
hal-00703207v1
Rapport
Claire Dross, Sylvain Conchon, Andrei Paskevich. Reasoning with Triggers [Research Report] RR-7986, INRIA. 2012, pp.29 |
||
|
hal-01162661v2
Communication dans un congrès
Martin Clochard, Jean-Christophe Filliâtre, Andrei Paskevich. How to avoid proving the absence of integer overflows Arie Gurfinkel and Sanjit A. Seshia. 7th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2015, San Francisco, CA, United States. 7th Working Conference on Verified Software: Theories, Tools, and Experiments. <http://verifun.eecs.berkeley.edu/vstte15/> |
||
|
hal-00913431v1
Communication dans un congrès
Martin Clochard, Claude Marché, Andrei Paskevich. Verified Programs with Binders Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ACM Press, 2014 |
||
|
inria-00591414v4
Rapport
François Bobot, Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language [Research Report] 2011 |
||
|
hal-00790310v1
Communication dans un congrès
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Why3: Shepherd Your Herd of Provers Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64, 2011 |
||
|
inria-00439232v2
Rapport
Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform [Research Report] RR-7128, INRIA. 2009 |
||
|
hal-00822856v1
Autre publication
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. The Why3 platform 0.81 Tutorial and Reference Manual. 2013 |
||
|
hal-00798777v1
Communication dans un congrès
Jean-Christophe Filliâtre, Andrei Paskevich, Aaron Stump. The 2nd Verified Software Competition: Experience Report Vladimir Klebanov, Bernhard Beckert, Armin Biere, Geoff Sutcliffe. COMPARE 2012, Comparative Empirical Evaluation of Reasoning Systems, 1st Intl. Workshop, Jun 2012, Manchester, United Kingdom. CEUR Workshop Proceedings, 873, pp.36-49, 2012, CEUR Workshop Proceedings; COMPARE 2012, Comparative Empirical Evaluation of Reasoning Systems. <http://ceur-ws.org/Vol-873/> |
||
|
hal-00789533v1
Communication dans un congrès
Jean-Christophe Filliâtre, Andrei Paskevich. Why3 -- Where Programs Meet Provers ESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy. Springer, 7792, 2013, LNCS; Proceedings of the 22nd European Symposium on Programming} |
||
|
hal-00967132v1
Article dans une revue
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Let's Verify This with Why3 Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727 |
||
|
hal-00873187v3
Communication dans un congrès
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. The Spirit of Ghost Code CAV 2014, Computer Aided Verification - 26th International Conference, Jul 2014, Vienna Summer Logic 2014, Austria. Computer Aided Verification - 26th International Conference, 2014, Held as Part of the Vienna Summer of Logic, 2014, Vienna, Austria, July 18-22, 2014. Proceedings, <http://cavconference.org/> |
||
|
hal-00875395v1
Communication dans un congrès
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. Preserving User Proofs Across Specification Changes Ernie Cohen and Andrey Rybalchenko. Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. Springer, 8164, pp.191-201, 2013 |
||
|
hal-01396864v1
Article dans une revue
Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. The Spirit of Ghost Code Formal Methods in System Design, Springer Verlag, 2016, 48 (3), pp.152-174. <10.1007/s10703-016-0243-x> |
||
|
hal-01221066v1
Article dans une revue
Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich. Adding Decision Procedures to SMT Solvers using Axioms with Triggers Journal of Automated Reasoning, Springer Verlag, 2016, 56 (4), pp.387-457. <10.1007/s10817-015-9352-2> |
||
|
|
||