HOL-OCL - A proof system for UML/OCL
Date of the last release: 15 August 2017

Person in charge : WOLFF Burkhart


HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as a shallow embedding of OCL into the Higher-order Logic (HOL) instance of the interactive theorem prover Isabelle. HOL-OCL is developed by Achim D. Brucker and Burkhart Wolff.

More information: http://www.brucker.ch/projects/hol-ocl/

Software - Licence : GPL



Research activities
  Formalisation of (Specification and Programming) Languages in Proof Assistants

Members
  WOLFF Burkhart

Group
  Verification of Algorithms, Languages and Systems

CODALAB
Codalab

DNADNA
Deep Neural Architectures for DNA

CARTOLABE
CARTOLABE