@string{MIT="MIT Press"}

@inproceedings{BerghoferN-SEFM04,author={Stefan Berghofer and Tobias Nipkow},
title={Random Testing in {Isabelle/HOL}},
booktitle={Software Engineering and Formal Methods (SEFM 2004)},
editor={J. Cuellar and Z. Liu},
year=2004,pages={230--239},publisher={IEEE Computer Society}}

@book{Jackson06,author={Daniel Jackson},
title={Software Abstractions. Logic, Language, and Analysis},
publisher=MIT,year=2006}

@inproceedings{Nipkow-TYPES02,author={Tobias Nipkow},
title={{Structured Proofs in Isar/HOL}},
booktitle={Types for Proofs and Programs (TYPES 2002)},
editor={H. Geuvers and F. Wiedijk},
year=2003,publisher=Springer,series=LNCS,volume=2646,pages={259-278}}

@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{Nipkow-ICTAC06,author={Tobias Nipkow},
title={Verifying a Hotel Key Card System},
booktitle={Theoretical Aspects of Computing (ICTAC 2006)},
editor={K. Barkaoui and A. Cavalcanti and A. Cerone},
publisher=Springer,series=LNCS,year=2006,
note={Invited paper}}

@article{Paulson-JCS98,author="Lawrence C. Paulson",
title="The inductive approach to verifying cryptographic protocols",
journal="J. Computer Security",year=1998,volume=6,pages="85--128"}

@article{MengQP-IC,author="Jia Meng and Claire Quigley and Lawrence C. Paulson",
title="Automation for Interactive Proof: First Prototype",
journal="Information and Computation",note="In press"}

@inproceedings{Weber05bounded,
  author    = {Tjark Weber},
  title     = {Bounded Model Generation for {Isabelle/HOL}},
  editor    = {W. Ahrendt and P. Baumgartner and H. de Nivelle and S. Ranise and C. Tinelli},
  booktitle = {Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 2004)},
  volume    = {125(3)},
  series    = {Electronic Notes in Theoretical Computer Science},
  pages     = {103--116},
  year      = {2005}
}

@phdthesis{Wenzel-PhD,author={Markus Wenzel},title={Isabelle/Isar --- A
Versatile Environment for Human-Readable Formal Proof Documents},
school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
year=2002,
note={\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}
