Identifiants chercheur

  • IdHAL : tertium

Widget extérieur

Nombre de documents

19


Article dans une revue3 documents

  • 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>. <hal-01221066>
  • 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-01396864>
  • 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-00967132>

Communication dans un congrès10 documents

  • 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-01162661v2>
  • 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-01067197>
  • Martin Clochard, Claude Marché, Andrei Paskevich. Verified Programs with Binders. Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ACM Press, 2014. <hal-00913431>
  • 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-00873187v3>
  • 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-00789533>
  • 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-00875395>
  • 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. <hal-00825086>
  • 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-00798777>
  • 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. <hal-00790310>
  • Evelyne 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>. <inria-00535655>

Autre publication1 document

  • François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. The Why3 platform 0.81. Tutorial and Reference Manual. 2013. <hal-00822856>

Pré-publication, Document de travail2 documents

  • Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. A Pragmatic Type System for Deductive Verification. 2016. <hal-01256434v3>
  • Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich. Adding Decision Procedures to SMT Solvers using Axioms with Triggers. 2013. <hal-00915931>

Rapport3 documents

  • Claire Dross, Sylvain Conchon, Andrei Paskevich. Reasoning with Triggers. [Research Report] RR-7986, INRIA. 2012, pp.29. <hal-00703207>
  • François Bobot, Andrei Paskevich. Expressing Polymorphic Types in a Many-Sorted Language. [Research Report] 2011. <inria-00591414v4>
  • Andrei Paskevich. Algebraic types and pattern matching in the logical language of the Why verification platform. [Research Report] RR-7128, INRIA. 2009. <inria-00439232v2>