@book{LNCS2283,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{ArkoudasETAL04VerifyingFileSystemImplementationICFEM,
  author =       {Konstantine Arkoudas and Karen Zee and Viktor Kuncak and Martin Rinard},
  title =        {Verifying a File System Implementation},
  booktitle =    {Sixth International Conference on Formal Engineering Methods (ICFEM'04)},
  series = {LNCS},  
  volume = {3308},
  year =         2004,
  address =      {Seattle},
  month =        {Nov 8-12, 2004}
}

@article{mckusick84fast,
    author = {Marshall K. McKusick and William N. Joy and Samuel J. Leffler and Robert S. Fabry},
    title = {A Fast File System for {UNIX}},
    journal = {Computer Systems},
    volume = {2},
    number = {3},
    pages = {181-197},
    year = {1984}}

@article{thompson78unix,
    author = {K. Thompson},
    title = {{UNIX} Implementation},
    journal = {The Bell System Technical Journal},
    volume = {57},
    number = {6 (part 2)},
    month = {},
    year = {1978}}

@Book{RoeverEngelhardt98DataRefinement,
  author =       {Willem-Paul de Roever and Kai Engelhardt},
  title =        {Data Refinement: Model-oriented proof methods and their comparison},
  publisher =    CUP,
  year =         1998,
  volume =       47,
  series =       {Cambridge Tracts in Theoretical Computer Science},
  issbn = 0521641705
}
