HOL-OCL enables the formal analysis of UML/OCL models by addressing two key issues: first, it provides a formal semantics that aims for standard compliance (e.g., a four-valued logic) and, second, it is verification environment for UML/OCL.


HOL-OCL is both a formal semantics of the Object Constraint Language (OCL) and UML class models expressed in terms of higher-order logic (i.e., as an shallow embedding in Isabelle/HOL) and an interactive proof environment for UML/OCL.

Analysing a simple bank example using HOL-OCL 2.0.
Analysing a simple bank example using HOL-OCL 2.0.

HOL-OCL is jointly developed by the Software Assurance & Security Research Team at the University of Sheffield, UK and the Verified Algorithms, Languages and Systems team at the LRI (CNRS and University of Paris-Sud), France.

HOL-OCL is free software. For more information, please visit the HOL-OCL home page.

In the context of HOL-OCL we provide a collection of UML/OCL examples as well as su4sml, an SML repository for managing (Secure)UML/OCL models. Both are available in the HOL-OCL organization of our code repository.

Important Publications

1. Brucker, A. D., Tuong, F., and Wolff, B. “Featherweight Ocl: A Proposal for a Machine-Checked Formal Semantics for Ocl 2.5Archive of Formal Proofs (2014): URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2014

2. Brucker, A. D. and Wolff, B. “Semantics, Calculi, and Analysis for Object-Oriented Specificationsj-acta-informatica 46, no. 4 (2009): 255–284. doi:10.1007/s00236-009-0093-8, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-semantics-2009

3. Brucker, A. D. and Wolff, B. “An Extensible Encoding of Object-Oriented Data Models in Holj-ar 41, no. 3 (2008): 219–249. doi:10.1007/s10817-008-9108-3, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b

4. Brucker, A. D. “An Interactive Proof Environment for Object-Oriented Specifications” (2007): URL: http://www.brucker.ch/bibliography/abstract/brucker-interactive-2007