2013-other.bib
@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}}
@unpublished{filliatre13digicosme,
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,
\url{https://usr.lmf.cnrs.fr/~jcf/digicosme-spring-school-2013/}}
}
@unpublished{dross13,
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}
}
@proceedings{itp13,
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}
}