2012-report.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib -q -oc 2012-report.cite -ob 2012-report.bib -c 'year = 2012 and topics : "team" and ($type="techreport" or $type="manual" or $type="mastersthesis")' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}

@manual{why3manual072,
  title = {The Why3 platform, version 0.72},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.72},
  month = may,
  year = 2012,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf},
  rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf}}
}

@manual{why3manual073,
  title = {The Why3 platform, version 0.73},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.73},
  month = jul,
  year = 2012,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf},
  rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf}}
}

@manual{why3manual080,
  title = {The Why3 platform, version 0.80},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.80},
  month = oct,
  year = 2012,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf},
  note = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}},
  rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}}
}

@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}
}

@techreport{blanchette12tr,
  author = {Jasmin C. Blanchette and Andrei Paskevich},
  title = {{TFF1}: The {TPTP} typed first-order form with rank-1 polymorphism},
  institution = {Tech. Univ. Munich},
  year = 2012,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  url = {http://www21.in.tum.de/~blanchet/tff1spec.pdf},
  note = {\url{http://www21.in.tum.de/~blanchet/tff1spec.pdf}}
}

@techreport{marche12rr,
  title = {Weakest Precondition Calculus, revisited using {Why3}},
  author = {Claude March\'e and Asma Tafat},
  type = {Research Report},
  institution = {INRIA},
  number = {RR-8185},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  year = 2012,
  month = dec,
  topics = {team},
  hal = {http://hal.inria.fr/hal-00766171},
  pdf = {http://hal.inria.fr/hal-00766171/PDF/RR-8185.pdf}
}