FDR Documentation

Welcome to the documentation for FDR 4.2.

FDR is a refinement checker for the process algebra CSP. It allows processes to be defined in a machine-readable version of CSP, CSPM, and is then able to check various assertions about these processes. FDR includes two main tools:

It also includes a number of utility tools:

The documentation is organised into four main sections.