FDR3 --- A Modern Refinement Checker for CSP

Thomas Gibson-Robinson ( University of Oxford )

FDR3 is a complete rewrite of the CSP refinement checker FDR2, incorporating a significant number of enhancements. In this talk I will give a brief overview of the new features of FDR3, and will then concentrate on describing the implementation of some of the FDR3 internals. This will include the new multi-core refinement-checking algorithm that is able to achieve a near linear speed up as the number of cores increases, and the new algorithm that FDR3 uses to construct its internal representation of CSP processes.