@InProceedings{Reus:2001:FASE,
  author =       "Bernhard Reus and Martin Wirsing and Rolf Hennicker",
  title =        "A Hoare Calculus for Verifying Java Realizations of
                  {OCL}-Constrained Design Models",
  pages =        "300--317",
  booktitle =    "Fundamental Approaches to Software Engineering, 4th
                  International Conference, FASE 2001, held as Part of the
                  Joint European Conferences on Theory and Practice of
                  Software, ETAPS 2001, Genova, Italy, April 2-6, 2001,
                  Proceedings",
  editor =       "Heinrich Hussmann",
  publisher =    "Springer",
  series =       "LNCS",
  volume =       "2029",
  year =         "2001",
}