HOL-OCL - A proof system for UML/OCL


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/

- Licence : GPL



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

Members
  WOLFF Burkhart

Group
  Verification of Algorithms, Languages and Systems

BSP++
The C++ Bulk Synchronous Parallelism Library

TAXOMAP ALIGNMENT
A prototype to automate semantic mappings between taxonomies

FR1155729
Procédé pour l’extinction de routeurs dans un réseau de communications et routeur mettant en œuvre ce procédé