hubert.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc hubert.cite -ob hubert.bib -c 'author : "Thierry Hubert\|T. Hubert"' /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}}
@misc{Caduceus,
  title = {The {Caduceus} tool for the verification of {C} programs},
  author = {Jean-Christophe Filli\^atre and Thierry Hubert and Claude March\'e},
  note = {\url{http://caduceus.lri.fr/}}
}
@inproceedings{couchot07ftp,
  author = {Jean-Fran\c{c}ois Couchot and Thierry Hubert},
  title = {{A Graph-based Strategy for the Selection of Hypotheses}},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {FTP},
  booktitle = {FTP 2007 - International Workshop on
                   First-Order Theorem Proving},
  address = {Liverpool, UK},
  month = sep,
  year = 2007,
  pages = {},
  x-pdf = {http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf},
  url = {http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf},
  abstract = {In previous works on verifying
C programs by deductive approaches based on SMT provers,
we proposed the heuristic of separation analysis to handle the most
difficult problems.
Nevertheless, this heuristic is not sufficient when applied on
industrial C programs:
it remains some Verification  Conditions (VCs) that cannot be decided
by any SMT prover, mainly due to their size.
This work presents a strategy to select relevant hypotheses
in each VC.
The relevance of an hypothesis is the combination of
two separated dependency analysis
obtained by some graph traversals.
The approach is applied on a benchmark issued from
an industrial program verification.
}
}
@mastersthesis{hubert04dea,
  author = {Thierry Hubert},
  title = {{Certification des preuves de terminaison en Coq}},
  type = {Rapport de {DEA}},
  year = 2004,
  month = sep,
  school = {Universit{\'e} Paris 7},
  topics = {team, lri},
  note = {\url{http://www.lri.fr/~marche/hubert04rr.ps}},
  url = {http://www.lri.fr/~marche/hubert04rr.ps}
}
@unpublished{hubert05,
  author = {Thierry Hubert and Claude March\'e},
  title = {A case study of {C} source code verification: the {Schorr}-{Waite} algorithm},
  year = 2005,
  url = {http://www.lri.fr/~marche/SchorrWaite.ps}
}
@inproceedings{hubert05sefm,
  author = {Thierry Hubert and Claude March\'e},
  topics = {team},
  title = {A case study of {C} source code verification: the {Schorr-Waite} algorithm},
  crossref = {sefm05},
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~marche/hubert05sefm.ps},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {SEFM}
}
@techreport{hubert07,
  author = {Thierry Hubert and Claude March\'e},
  title = {Separation Analysis for Deductive Verification},
  institution = {Universit\'e Paris XI},
  year = 2007,
  note = {\url{http://www.lri.fr/~marche/separation.pdf}},
  url = {http://www.lri.fr/~marche/separation.pdf},
  x-pdf = {http://www.lri.fr/~marche/separation.pdf}
}
@inproceedings{hubert07hav,
  author = {Thierry Hubert and Claude March\'e},
  title = {Separation Analysis for Deductive Verification},
  booktitle = {Heap Analysis and Verification (HAV'07)},
  year = 2007,
  address = {Braga, Portugal},
  month = mar,
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  pages = {81--93},
  url = {http://www.lri.fr/~marche/hubert07hav.pdf},
  x-pdf = {http://www.lri.fr/~marche/hubert07hav.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {HAV}
}
@phdthesis{hubert2008these,
  author = {Thierry Hubert},
  title = {Analyse Statique et preuve de Programmes Industriels Critiques},
  school = {Universit{\'e} Paris-Sud},
  year = 2008,
  type = {Th{\`e}se de Doctorat},
  month = jun,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport},
  url = {http://www.lri.fr/~marche/hubert08these.pdf}
}
@proceedings{sefm05,
  title = {Software Engineering and Formal Methods},
  year = 2005,
  booktitle = {3rd IEEE International Conference on Software Engineering
and Formal Methods (SEFM'05)},
  address = {Koblenz, Germany},
  editor = {Bernhard K. Aichernig and Bernhard Beckert},
  publisher = {{IEEE} Comp. Soc. Press},
  month = sep
}