@InCollection{	  brucker.ea:hol-ocl:2008,
  abstract	= {We present the theorem proving environment HOL-OCL that is
		  integrated in a MDE framework. HOL-OCL allows to reason
		  over UMLclass models annotated with OCL specifications.
		  Thus, HOL-OCL strengthens a crucial part of the UML to an
		  object-oriented formal method. HOL-OCL provides several
		  derived proof calculi that allow for formal derivations
		  establishing the validity of UML/OCL formulae. These
		  formulae arise naturally when checking the consistency of
		  class models, when formally refining abstract models to
		  more concrete ones or when discharging side-conditions from
		  model-transformations.},
  keywords	= {HOL-OCL, UML, OCL, Formal Methods, Theorem Proving,
		  Refinement},
  location	= {Budapest, Hungary},
  author	= {Achim D. Brucker and Burkhart Wolff},
  booktitle	= {Fundamental Approaches to Software Engineering
		  {(FASE08)}},
  talk		= {brucker.ea:hol-ocl:2008},
  language	= {USenglish},
  publisher	= {Springer-Verlag},
  address	= {Heidelberg},
  series	= {Lecture Notes in Computer Science},
  number	= {4961},
  doi		= {10.1007/978-3-540-78743-3_8},
  pages		= {97--100},
  editor	= {Jos{\'e} Fiadeiro and Paola Inverardi},
  title		= {{HOL-OCL} -- {A Formal Proof Environment for
		  {UML}/{OCL}}},
  categories	= {holocl},
  classification= {conference},
  areas		= {formal methods, software},
  year		= {2008},
  pdf		= {http://www.brucker.ch/bibliography/download/2008/brucker.ea-hol-ocl-2008.pdf},
  public	= {yes},
  url		= {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008}
		  
}