FDR is a tool for analyzing programs written in Hoare’s CSP notation.
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.