2016-report.bib

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

@comment{{Command line: /usr/bin/bib2bib -q -oc 2016-report.cite -ob 2016-report.bib -c 'year = 2016 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{CoqManualV86,
  author = {{The {Coq} Development Team}},
  title = {{The Coq Proof Assistant Reference Manual -- Version V8.6}},
  year = 2016,
  note = {\url{http://coq.inria.fr}},
  url = {http://coq.inria.fr},
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL EXT},
  x-type = {manuel},
  x-support = {diffusion}
}

@techreport{hauzar16rr,
  topics = {team},
  title = {Counterexamples from proof failures in the {SPARK} program verifier},
  author = {Hauzar, David and March{\'e}, Claude and Moy, Yannick},
  hal = {https://hal.inria.fr/hal-01271174},
  type = {Research Report},
  number = {RR-8854},
  institution = {Inria Saclay Ile-de-France},
  year = 2016,
  month = feb
}

@techreport{gondelman16reg,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and L\'eon
            Gondelman and Andrei Paskevich},
  title = {A Pragmatic Type System for Deductive Verification},
  type = {Research Report},
  institution = {Universit\'e Paris Sud},
  year = 2016,
  abstract = { In the context of deductive verication, it is customary
                  today to handle programs with pointers using either
                  separation logic, dynamic frames, or explicit memory
                  models. Yet we can observe that in numerous
                  programs, a large amount of code ts within the scope
                  of Hoare logic, provided we can statically control
                  aliasing. When this is the case, the code
                  correctness can be reduced to simpler verication
                  conditions which do not require any explicit memory
                  model. This makes verication conditions more
                  amenable both to automated theorem proving and to
                  manual inspection and debugging. In this paper, we
                  devise a method of such static aliasing control for
                  a programming language featuring nested data
                  structures with mutable components. Our solution is
                  based on a type system with singleton regions and
                  eects, which we prove to be sound.},
  hal = {https://hal.archives-ouvertes.fr/hal-01256434v3},
  note = {\url{https://hal.archives-ouvertes.fr/hal-01256434v3}}
}

@techreport{chen16rr,
  topics = {team},
  title = {A Formal Proof of a {Unix} Path Resolution Algorithm},
  author = {Ran Chen and Martin Clochard and Claude March\'e},
  hal = {https://hal.inria.fr/hal-01406848},
  type = {Research Report},
  number = {RR-8987},
  institution = {Inria},
  year = 2016,
  month = dec
}