@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2013-other.cite -ob 2013-other.bib -c 'year = 2013 and topics : "team" and $type<>"article" and $type<>"inproceedings" and $type<>"book" and $type<>"inbook" and $type<>"incollection" and $type<>"phdthesis" and $type<>"techreport" and $type<>"manual" and $type<>"mastersthesis"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
  author = {Jean-Christophe Filli\^atre},
  topics = {team},
  keywords = {Why3},
  title = {Deductive Program Verification with {Why3}},
  year = 2013,
  note = {Lecture notes for the First {DigiCosme} Spring School,
  topics = {team},
  hal = {http://hal.inria.fr/hal-00915931},
  title = {Adding Decision Procedures to {SMT} Solvers using Axioms with Triggers},
  author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes and Paskevich, Andrei},
  abstract = {SMT solvers are efficient tools to decide the
                  satisfiability of ground formulas, including a
                  number of built-in theories such as congruence,
                  linear arithmetic, arrays, and bit-vectors. Adding a
                  theory to that list requires delving into the
                  implementation details of a given SMT solver, and is
                  done mainly by the developers of the solver
                  itself. For many useful theories, one can
                  alternatively provide a first-order
                  axiomatization. However, in the presence of
                  quantifiers, SMT solvers are incomplete and exhibit
                  unpredictable behavior. Consequently, this approach
                  can not provide us with a complete and terminating
                  treatment of the theory of interest. In this paper,
                  we propose a framework to solve this problem, based
                  on the notion of instantiation patterns, also known
                  as triggers. Triggers are annotations that suggest
                  instances which are more likely to be useful in
                  proof search. They are implemented in all SMT
                  solvers that handle first-order logic and are
                  included in the SMT-LIB format. In our framework,
                  the user provides a theory axiomatization with
                  triggers, along with a proof of completeness and
                  termination properties of this axiomatization, and
                  obtains a sound, complete, and terminating solver
                  for her theory in return. We describe and prove a
                  corresponding extension of the traditional Abstract
                  DPLL Modulo Theory framework. Implementing this
                  mechanism in a given SMT solver requires a one-time
                  development effort. We believe that this effort is
                  not greater than that of adding a single decision
                  procedure to the same SMT solver. We have
                  implemented the proposed extension in the Alt-Ergo
                  prover and we discuss some implementation details in
                  the paper. To show that our framework can handle
                  complex theories, we prove completeness and
                  termination of a feature-rich axiomatization of
                  doubly-linked lists. Our tests show that our
                  approach results in a better performance of the
                  solver on goals that stem from the verification of
                  programs manipulating doubly-linked lists.},
  language = {Anglais},
  affiliation = {TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , AdaCore SAS - AdaCore SAS},
  year = 2013,
  pdf = {http://hal.inria.fr/hal-00915931/PDF/dross-article.pdf},
  note = {Submitted}
  hal_id = {hal-00908865},
  url = {http://hal.inria.fr/hal-00908865},
  topics = {team},
  title = {{Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings.}},
  editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
  language = {Anglais},
  affiliation = {CELTIQUE - INRIA - IRISA , TOCCATA - INRIA - Laboratoire de Recherche en Informatique - LRI},
  publisher = {Springer},
  pages = {500},
  volume = {7998},
  series = {Lecture Notes in Computer Science},
  audience = {internationale },
  doi = {10.1007/978-3-642-39634-2},
  year = {2013}