2016-journal.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2016-journal.cite -ob 2016-journal.bib -c 'year = 2016 and topics : "team" and $type="article"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@article{BLM14mscs,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Formalization of Real Analysis: A Survey of Proof Assistants and Libraries},
year = {2016},
hal = {http://hal.inria.fr/hal-00806920},
journal = {Mathematical Structures in Computer Science},
topics = {team}
}
@article{dross16jar,
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-01221066},
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.},
year = 2016,
journal = {Journal of Automated Reasoning},
volume = 56,
number = 4,
pages = {387--457}
}
@article{gondelman16fmsd,
author = {Jean-Christophe Filli\^atre and L\'eon
Gondelman and Andrei Paskevich},
title = {The Spirit of Ghost Code},
journal = {Formal Methods in System Design},
publisher = {Springer},
year = 2016,
volume = 48,
number = 3,
pages = {152--174},
issn = {1572-8102},
doi = {10.1007/s10703-016-0243-x},
topics = {team},
hal = {https://hal.archives-ouvertes.fr/hal-01396864v1},
keywords = {Why3},
type_publi = {irevcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {revue},
x-editorial-board = {yes},
abstract = {
In the context of deductive program verification, ghost code is part
of the program that is added for the purpose of specification.
Ghost code must not interfere with regular code, in the sense that
it can be erased without observable difference in the program outcome.
In particular, ghost data cannot participate in regular
computations and ghost code cannot mutate regular data or diverge.
The idea exists in the folklore since the early notion of auxiliary
variables and is implemented in many state-of-the-art program
verification tools. However, a rigorous definition and treatment of
ghost code is surprisingly subtle and few formalizations exist.
In this article, we describe a simple ML-style programming language
with mutable state and ghost code. Non-interference is ensured by a
type system with effects, which allows, notably, the same data types
and functions to be used in both regular and ghost code.
We define the procedure of ghost code erasure and we prove its
safety using bisimulation.
A similar type system, with numerous extensions which we briefly discuss,
is implemented in the program verification environment Why3.
}
}
@article{martindorel15jara,
topics = {team},
title = {Proving Tight Bounds on Univariate Expressions with Elementary Functions in {Coq}},
author = {Martin-Dorel, {\'E}rik and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-01086460},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
year = 2016,
doi = {10.1007/s10817-015-9350-4},
keywords = {Coq proof assistant ; formal proof ; decision procedure ; interval arithmetic ; floating-point arithmetic ; nonlinear arithmetic}
}
@article{acar:hal-01409069,
topics = {team},
title = {Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages},
author = {Acar, Umut A and Chargu{\'e}raud, Arthur and Rainey, Mike},
hal = {https://hal.inria.fr/hal-01409069},
journal = {Journal of Functional Programming},
publisher = {Cambridge University Press},
volume = 26,
year = 2016,
month = nov,
doi = {10.1017/S0956796816000101}
}