img img

A logic-based library for correct-by-construction process modelling and composition.

Read the DocsSource


This is a logic-based library for the interactive theorem prover HOL Light that allows for rigorous, formally verified process specification and composition. The resulting workflows are correct-by-construction with the following verified properties:

The constructed workflows can be exported either for visualization using the PiVizTool or as Scala code for execution using the PEW engine.

Key Features


The reasoner can run in 2 modes:



Petros Papapanagiotou - Home page - Email - Twitter


A big thank you to the following contributors in order of appearance:

Groups & Organizations

Artificial Intelligence Modelling Lab
Artificial Intelligence and its Applications Institute
School of Informatics, University of Edinburgh


Please cite the following publication in reference to this project:

Sample of other relevant references:


Distributed under the Apache 2.0 license. See LICENSE for more information.

Copyright © 2009-2021 The University of Edinburgh and contributors