@InCollection{	  bohme.ea:hol-boogie:2008,
  abstract	= {Boogie is a program verification condition generator for
		  animperative core language. It has front-ends for the
		  programming languagesC# and C enriched by annotations in
		  first-order logic.Its verification conditions — constructed
		  via a wp calculus from theseannotations — are usually
		  transferred to automated theorem proverssuch as Simplify or
		  Z3. In this paper, however, we present a
		  proof-environment,HOL-Boogie, that combines Boogie with the
		  interactivetheorem prover Isabelle/HOL. In particular, we
		  present specific techniquescombining automated and
		  interactive proof methods for code-verification.We will
		  exploit our proof-environment in two ways: First, we
		  present scenariosto \"debug\" annotations (in particular:
		  invariants) by interactiveproofs. Second, we use our
		  environment also to verify \"background theories\",i.e.
		  theories for data-types used in annotations as well as
		  memoryand machine models underlying the verification method
		  for C.},
  address	= {Montreal, Canada},
  author	= {Sascha B\"ohme and Rustan Leino and Burkhart Wolff},
  booktitle	= {21th International Conference on Theorem proving in
		  Higher-Order Logics (TPHOLs 2008)},
  copyright	= {\copyright Springer-Verlag},
  editor	= {Sofiene Tahar and Otmane Ait Mohamed and C{\'e}sar
		  Mu{\~n}oz},
  language	= {USenglish},
  pdf		= {papers/2008/boehme_tphols_2008.pdf},
  publisher	= {Springer-Verlag},
  series	= {LNCS 5170},
  title		= {HOL-Boogie — An Interactive Prover for the Boogie Program
		  Verifier},
  year		= 2008,
  user		= {lukasbru}
}