img img

A diagrammatic tool for formally verified process modelling and composition.

Client DocsServer DocsSource


The WorkflowFM Composer consists of a Java-based server and GUI for formally verified process composition using the WorkflowFM Reasoner. It provides a visual, diagrammatic interface to specify processes based on their input and output resources, and compose them together to form more complex workflows.

Actions in the GUI of the Client are sent to the Server, which in turn is able to interact directly with the Reasoner. The Reasoner then performs the necessary logic-based inference within the rigorous environment of the HOL Light theorem prover.

The end result is a composite process that is provably correct and has the following properties:

Key Features



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