dross.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc dross.cite -ob dross.bib -c 'author : "dross"' /home/marche/biblio/abbrevs.bib /home/marche/biblio/demons.bib /home/marche/biblio/demons2.bib /home/marche/biblio/demons3.bib /home/marche/biblio/team.bib /home/marche/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{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}
}
@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}
}