@InProceedings{	  sprenger.ea:monad-based:2007-b,
  abstract	= {We present an advanced modeling and verification toolbox
		  for functional programs with state and exceptions. The
		  toolbox integrates an extensible, monad-based, component
		  model, a monad-based Hoare logic and weakest pre-condition
		  calculus, and proof systems for temporal logic and
		  bisimilarity. It is implemented in Isabelle/HOL using
		  shallow embeddings and incorporates as much modeling and
		  reasoning power as possible from Isabelle/HOL. We have
		  validated the toolbox's usefulness in a substantial
		  security protocol verification project.},
  author	= {Christoph Sprenger and David Basin},
  booktitle	= {Theorem Proving in Higher-Order Logics (TPHOLs)},
  editor	= {K. Schneider and J. Brandt},
  language	= {USenglish},
  pages		= {301--317},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  title		= {A monad-based modeling and verification toolbox with
		  application to security protocols},
  volume	= 4732,
  year		= 2007
}