Dr Petros Papapanagiotou

Senior Scala Engineer

WorkflowFM Reasoner

The WorkflowFM Reasoner is a logic-based library for correct-by-construction process modelling and composition.

It is available under the Apache 2.0 License on GitHub: https://github.com/workflowfm/workflowfm-reasoner

Website and documentation is available here: http://docs.workflowfm.com/workflowfm-reasoner/


It is implemented as 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