@InProceedings{ brucker.ea:formal:2008, abstract = {We present the theorem proving environment HOL-OCL that is integrated in a MDE framework. HOL-OCL allows to reason over \acs{uml} class models annotated with \acs{ocl} specifications. Thus, HOL-OCL strengthens a crucial part of the UML to an object-oriented formal method. \holocl 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.}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Proceedings of Formal Aspects of Software Engineering (FASE 2008)}, isbn = {0302-9743}, language = {USenglish}, pages = {97--101}, pdf = {papers/2008/2008-fase-hol-ocl.pdf}, publisher = {Springer Berlin / Heidelberg}, series = {Lecture Notes in Computer Science}, title = {A Formal Proof Environment for UML/OCL}, volume = 4961, year = 2008, user = {lukasbru} }