Quelle  root.bib

%----------------------------------------------------------------------


@string{AI="Acta Informatica"}
@string{AP="Academic Press"}
@string{CACM="Communications of the ACM"}
@string{CUP="Cambridge University Press"}
@string{FAC="Formal Aspects of Computing"}
@string{IC="Information and Computation"}
@string{IPL="Information Processing Letters"}
@string{JAR="J. Automated Reasoning"}
@string{JCSS="J. Computer and System Sciences"}
@string{JFP="J. Functional Programming"}
@string{JSC="J. Symbolic Computation"}
@string{JSL="J. Symbolic Logic"}
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
%@string{LNCS="LNCS"}
@string{LNAI="Lect.\ Notes in Art.\ Int."}
@string{OUP="Oxford University Press"}
@string{MIT="MIT Press"}
@string{PH="Prentice-Hall"}
@string{SCP="Science of Computer Programming"}
@string{Springer="Springer-Verlag"}
%@string{Springer="Springer"}
@string{TCS="Theoretical Computer Science"}
@string{TOPLAS="ACM Trans.\ Programming Languages and Systems"}

@inproceedings{Ballarin-04-locales,
  author = "Clemens Ballarin",
  title = "Locales and Locale Expressions in {I}sabelle/{I}sar",
  pages = "34-50",
  crossref = "BerardiEtAl2004"
}

@proceedings{BerardiEtAl2004,
  editor = "Stefano Berardi and  Mario Coppo and Ferruccio Damiani",
  title = "{T}ypes for Proofs and Programs: International Workshop,
{TYPES} 2003, {Torino, Italy, April 30--May 4, 2003}, Selected Papers",
  booktitle = "Types for Proofs and Programs: International Workshop,
{TYPES} 2003, {Torino, Italy, April 30--May 4, 2003}, Selected Papers",
  publisher = Springer,
  series = LNCS,
  number = "3085",
  year = 2004
}

@Book{Nipkow-02-hol,
 author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher=Springer,series=LNCS,volume=2283,year=2002,
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}

@InProceedings{NaraschewskiW-TPHOLs98,
author={Wolfgang Naraschewski and Markus Wenzel},
title=
{{O}bject-Oriented Verification based on Record Subtyping in Higher-Order Logic},
booktitle={Theorem Proving in Higher Order Logics:
11th International Conference, TPHOLs'98},
publisher=Springer,volume=1479,series=LNCS,year=1998}

@inproceedings{MehtaN-CADE03,author={Farhad Mehta and Tobias Nipkow},
title={Proving Pointer Programs in Higher-Order Logic},
booktitle="Automated Deduction --- CADE-19",editor="F. Baader",
year=2003,publisher=Springer,series=LNCS,volume={2741},pages={121--135}}

@phdthesis{Homeier-95-vcg,
  author = {Peter V. Homeier},
  title  = {Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures},
  school = {Department of Computer Science, University of California, Los Angeles},
  year = {1995},
}

@PhdThesis{Schirmer-PhD,
  author =   {Norbert Schirmer},
  title =   {Verification of Sequential Imperative Programs in {I}sabelle/{HOL}},
  school =   {Technische Universit\"at M\"unchen},
  year =   {2006},
  note = {Available from \url{http://mediatum2.ub.tum.de/doc/601799/601799.pdf}}
}

@inproceedings{Ortner-Schirmer-TPHOL05,
author={Veronika Ortner and Norbert Schirmer},
title={Verification of {BDD} Normalization},
pages={261--277},
crossref={TPHOL05}
}



@Proceedings{TPHOL05,
  editor={J. Hurd and T. Melham},
  title={Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005},
 booktitle={Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005},
  publisher=Springer,
  series=LNCS,
  volume=3603,
  year=2005,
}

@inproceedings{Leinenbach:SSV08-??,
AUTHOR = {Leinenbach, D. and Petrova, E.},
TITLE = {Pervasive Compiler Verification -- From Verified Programs to Verified Systems},
YEAR = {2008},
BOOKTITLE = {3rd intl Workshop on Systems Software Verification (SSV08), to appear},
PUBLISHER = {Elsevier Science B. V.},
}

@inproceedings{Alkassar:TACAS08-??,
AUTHOR = {Alkassar, E. and Schirmer, N. and Starostin, A.},
TITLE = {Formal Pervasive Verification of a Paging Mechanism},
YEAR = {2008},
SERIES = {LNCS},
BOOKTITLE = {14th intl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08), to appear},
PUBLISHER = {Springer},
}

@inproceedings{Tuch:separation-logic:2007,
  author = {Harvey Tuch and Gerwin Klein and Michael Norrish},
  title = {Types, Bytes, and Separation Logic},
  booktitle = {POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT
               symposium on Principles of programming languages},
  year = 2007,
  isbn = {1-59593-575-4},
  pages = {97--108},
  location = {Nice, France},
  doi = {http://doi.acm.org/10.1145/1190216.1190234},
  publisher = {ACM Press},
  address = {New York, NY, USA},
}