Quellcode-Bibliothek root.bib

@phdthesis{Grov09,
 Author = {Gudmund Grov},
 Month = {March},
 School = {Heriot-Watt University},
 Title = {{R}easoning about {C}orrectness {P}roperties of a {C}oordination {P}rogramming {L}anguage},
 Year = {2009}}

@inproceedings{Ehmety01,
 Author = {Sidi O. Ehmety and Lawrence C. Paulson},
 Booktitle = {Theorem Proving in Higher Order Logics},
 Editor = {Richard J. Boulton and Paul B. Jackson},
 Pages = {151--158},
 Title = {{R}epresenting {C}omponent {S}tates in {H}igher-{O}rder {L}ogic},
 Year = {2001}}

@inproceedings{Devillers97,
 Author = {Marco Devillers and David Griffioen and Olaf M\"{u}ller},
 Booktitle = {10th International Conference on Theorem Proving in Higher Order Logics},
 Editor = {Elsa L. Gunter and Amy P. Felty},
 Month = {August},
 Pages = {89--104},
 Publisher = {Springer},
 Series = {Lecture Notes in Computer Science},
 Title = {{P}ossibly {I}nfinite {S}equences in {T}heorem {P}rovers: {A} Comparative Study},
 Volume = {1275},
 Year = {1997}}

@article{Lamport94,
 Author = {Leslie Lamport},
 Journal = {{ACM} {T}ransactions on {P}rogramming {L}anguages and {S}ystems},
 Month = may,
 Number = {3},
 Pages = {872--923},
 Title = {{T}he {T}emporal {L}ogic of {A}ctions},
 Volume = {16},
 Year = {1994}}

@inproceedings{Wildmoser04,
 Author = {Martin Wildmoser and Tobias Nipkow},
 Booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2004)},
 Editor = {K. Slind and A. Bunker and G. Gopalakrishnan},
 Pages = {305-320},
 Publisher = {Springer},
 Series = {LNCS},
 Title = {{C}ertifying {M}achine {C}ode {S}afety: {S}hallow versus {D}eep {E}mbedding},
 Volume = 3223,
 Year = 2004}

@inproceedings{Merz99,
 Address = {Toulouse, France},
 Author = {Stephan Merz},
 Booktitle = {FM'99: {W}orld {C}ongress on {F}ormal {M}ethods},
 Editor = {J.M. Wing and J. Woodcock and J. Davies},
 Month = sep,
 Pages = {1226--1244},
 Publisher = {Springer-Verlag},
 Series = {Lecture Notes in Computer Science},
 Title = {{A} {M}ore {C}omplete {TLA}},
 Volume = 1709,
 Year = 1999}

@misc{Wenzel00b,
 Author = {Markus Wenzel},
 Month = May,
 Title = {{U}sing {A}xiomatic {T}ype {C}lasses in {I}sabelle},
 Year = {2000}}

@book{Lamport02,
 Address = {Reading, Massachusetts},
 Author = {Leslie Lamport},
 Publisher = {Addison-Wesley},
 Title = {Specifying Systems --- The TLA+ Language and Tools for Hardware and Software Engineers},
 Year = {2002}}

@unpublished{Merz98,
 Author = {Stephan Merz},
 Note = {http://www.pst.informatik.uni-muenchen.de/\~{}merz/isabelle/. Part of the Isabelle distribution.},
 Title = {{A}n {E}ncoding of {TLA} in {I}sabelle},
 Year = {1998}}

@InProceedings{chaudhuri:tlaps,
  author =       {Kaustuv Chaudhuri and Damien Doligez and Leslie Lamport and Stephan Merz},
  title =        {Verifying Safety Properties with the TLA\textsuperscript{+} Proof System},
  booktitle = {5th Intl. Joint Conf. Automated Reasoning (IJCAR 2010)},
  pages =     {142-148},
  year =      2010,
  editor =    {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
  volume =    6173,
  series =    {Lecture Notes in Computer Science},
  address =   {Edinburgh, UK},
  publisher = {Springer},
}