dross.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc dross.cite -ob dross.bib -c 'author : "dross"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{Summers10VMCAI,
author = {Alexander J. Summers and
Sophia Drossopoulou},
title = {Considerate Reasoning and the Composite Design Pattern},
booktitle = {VMCAI},
year = {2010},
pages = {328-344},
ee = {http://dx.doi.org/10.1007/978-3-642-11319-2_24},
crossref = {vmcai2010},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{dross16rssr,
author = {Claire Dross and Yannick Moy},
title = {Abstract Software Specifications and Automatic Proof of Refinement},
booktitle = {1st International Conference on Reliability, Safety and Security of Railway Systems },
year = 2016
}
@inproceedings{dross17nfm,
author = {Claire Dross and Yannick Moy},
title = {Auto-Active Proof of Red-Black Trees in SPARK},
booktitle = {NASA Formal Methods},
year = 2017
}
@inproceedings{dross20cav,
author = {Claire Dross and Johannes Kanig},
title = {Recursive Data Structures in SPARK},
booktitle = {Computer Aided Verification},
year = 2020
}
@inproceedings{Summers10iwaco09,
author = {Summers, Alexander J. and Drossopoulou, Sophia and M\"{u}ller, Peter},
title = {The Need for Flexible Object Invariants},
year = 2009,
isbn = 9781605585468,
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1562154.1562160},
doi = {10.1145/1562154.1562160},
abstract = {Specification and verification of object oriented programs usually features in some capacity the concept of an object invariant, used to describe the consistent states of an object. Unavoidably, an object's invariant will be broken at some points in its lifetime, and as a result, invariant protocols have been suggested, which prescribe the times at which object invariants may be broken, and the points at which they have to be re-established.The fact that currently available invariant protocols do not handle well some known examples, together with the fact that object invariants and invariant protocols can largely be encoded through methods' pre- and post- conditions has recently raised the question of whether they still have a role to play, or should be replaced by more explicit pre- and post-conditions for methods.In this paper we argue that invariant protocols express programmers' intuitions, lead to better design, allow more succinct specifications and proofs, and allow the expression of properties which involve many objects in a localised manner. In particular, the resulting verification conditions can be made simpler and more modular through the use of invariant-based reasoning.We also argue that even though encoding invariant protocols through methods' pre- and post-conditions is possible, such an encoding loses important information, and as a result makes specifications less explicit and program evolution (whereby the program evolves after the encoding has taken place) more error-prone. Finally, we show that such encodings often cannot express properties over inaccessible objects, whereas an appropriate invariant protocol can handle them simply.},
booktitle = {International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming},
articleno = 6,
numpages = 9,
location = {Genova, Italy},
series = {IWACO '09}
}
@inproceedings{dross11tap,
author = {Claire Dross and Jean-Christophe Filli\^atre and Yannick Moy},
title = {{Correct Code Containing Containers}},
booktitle = {5th International Conference on Tests and Proofs (TAP'11)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6706},
pages = {102--118},
year = 2011,
address = {Zurich},
month = jun,
url = {http://proval.lri.fr/publications/dross11tap.pdf},
hal = {http://hal.inria.fr/hal-00777683},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-equipes = {demons PROVAL ext},
x-cle-support = {TAP},
abstract = {
For critical software development, containers such as lists, vectors, sets or
maps are an attractive alternative to ad-hoc data structures based on
pointers.
As standards like DO-178C put formal verification and testing on an equal
footing, it is important to give users the ability to apply both to the
verification of code using containers.
In this paper,
we present a definition of containers whose aim is to facilitate their
use in certified software, using modern proof technology and novel
specification languages. Correct usage of containers and user-provided
correctness properties can be checked either by execution during testing
or by formal proof with an automatic prover.
We present a formal semantics for containers and an axiomatization of this
semantics targeted at automatic provers. We have proved in Coq that the
formal semantics is consistent and that the axiomatization thereof is
correct.}
}
@techreport{dross12rr,
title = {Reasoning with Triggers},
author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes
and Paskevich, Andrei},
abstract = {SMT solvers can decide the satisfiability of ground
formulas modulo a combination of built-in
theories. Adding a built-in theory to a given SMT
solver is a complex and time consuming task that
requires internal knowledge of the solver. However,
many theories can be easily expressed using
first-order formulas. Unfortunately, since universal
quantifiers are not handled in a complete way by SMT
solvers, these axiomatics cannot be used as decision
procedures. In this paper, we show how to extend a
generic SMT solver to accept a custom theory
description and behave as a decision procedure for
that theory, provided that the described theory is
complete and terminating in a precise sense. The
description language consists of first-order axioms
with triggers, an instantiation mechanism that is
found in many SMT solvers. This mechanism, which
usually lacks a clear semantics in existing
languages and tools, is rigorously defined here;
this definition can be used to prove completeness
and termination of the theory. We demonstrate on two
examples, how such proofs can be achieved in our
formalism.},
keywords = {Quantifiers, Triggers, SMT Solvers, Theories},
language = {English},
affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI},
pages = 29,
type = {Research Report},
institution = {INRIA},
number = {RR-7986},
year = 2012,
month = jun,
x-equipes = {demons PROVAL ext},
x-support = {rapport},
x-type = {article},
topics = {team},
hal = {http://hal.inria.fr/hal-00703207},
pdf = {http://hal.inria.fr/hal-00703207/PDF/RR-7986.pdf}
}
@inproceedings{dross12smt,
author = {Claire Dross and Sylvain Conchon and Johannes Kanig and Andrei Paskevich},
title = {Reasoning with Triggers},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-type = {article},
x-cle-support = {SMT},
crossref = {smt2012},
topics = {team}
}
@inproceedings{kanig12hilt,
topics = {team},
author = {Johannes Kanig and Edmond Schonberg and Claire Dross},
title = {{Hi-Lite}: the convergence of compiler technology and program
verification},
pages = {27--34},
editor = {Ben Brosgol and Jeff Boleng and S. Tucker Taft},
booktitle = {Proceedings of the 2012 ACM Conference on High Integrity
Language Technology, HILT '12},
address = {Boston, USA},
publisher = {ACM Press},
year = 2012
}
@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}
}
@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}
}
@phdthesis{dross14phd,
author = {Claire Dross},
title = {Generic Decision Procedures for Axiomatic First-Order Theories},
school = {Universit{\'e} Paris-Sud},
type = {Th{\`e}se de Doctorat},
hal = {http://tel.archives-ouvertes.fr/tel-01002190},
x-equipes = {demons ProVal Toccata},
x-support = {rapport},
x-type = {these},
topics = {team},
year = 2014,
month = apr
}
@techreport{dross15rr,
topics = {team},
title = {High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs},
author = {Dross, Claire and Fumex, Cl{\'e}ment and Gerlach, Jens and March{\'e}, Claude},
hal = {https://hal.inria.fr/hal-01238376},
type = {Research Report},
number = 8821,
institution = {Inria},
year = 2015,
month = dec
}
@inproceedings{fumex16nfm,
topics = {team},
author = {Fumex, Cl\'ement and Dross, Claire and Gerlach, Jens and March\'e, Claude},
title = {Specification and Proof of High-Level Functional Properties of Bit-Level Programs},
pages = {291--306},
crossref = {nfm16},
hal = {https://hal.inria.fr/hal-01314876}
}
@unpublished{jaloyan18,
topics = {team},
title = {Verification of Programs with Pointers in {SPARK}},
author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-01936105},
note = {working paper \url{https://hal.inria.fr/hal-01936105}},
year = 2018,
month = nov
}
@inproceedings{jaloyan20icfem,
topics = {team},
title = {Verification of Programs with Pointers in {SPARK}},
author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
hal = {https://hal.inria.fr/hal-03094566},
booktitle = {Formal Methods and Software Engineering (ICFEM)},
pages = {55--72},
year = 2020,
doi = {10.1007/978-3-030-63406-3\_4}
}
@proceedings{vmcai2010,
editor = {Gilles Barthe and
Manuel V. Hermenegildo},
title = {Verification, Model Checking, and Abstract Interpretation,
11th International Conference, VMCAI 2010, Madrid, Spain,
January 17-19, 2010. Proceedings},
booktitle = {VMCAI},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5944},
year = {2010},
isbn = {978-3-642-11318-5},
ee = {http://dx.doi.org/10.1007/978-3-642-11319-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{smt2012,
booktitle = {SMT workshop},
editor = {Pascal Fontaine and Amit Goel},
publisher = {LORIA},
url = {http://smt2012.loria.fr/},
year = 2012,
x-international-audience = {yes},
x-proceedings = {no},
address = {Manchester, UK}
}
@proceedings{nfm16,
booktitle = {8th NASA Formal Methods Symposium},
address = {Minneapolis, MN, USA},
audience = {internationale},
year = 2016,
month = jun,
editor = {Rayadurgam, Sanjai and Tkachuk, Oksana},
series = {Lecture Notes in Computer Science},
volume = {9690},
publisher = {Springer}
}