The CSP refinement checker, now with a new
lightning-fast multicore refinement-checking engine.

Download

FDR4 — The CSP Refinement Checker

FDR4 analyses programs written in CSPM, which combines the
operators of Hoare's CSP with a functional programming language. It also has support for analysing timed systems, via tock CSP.

N = 8

PHILNAMES = {0..N-1}
FORKNAMES = {0..N-1}

channel thinks, sits, eats, getsup : PHILNAMES

channel picks, putsdown : PHILNAMES.FORKNAMES

-- A philosopher thinks, sits down, picks up two forks,
-- eats, puts down forks and gets up, in an unending
-- cycle.

PHIL(i) =
  thinks.i -> sits!i -> picks!i!i ->
  picks!i!((i+1)%N) -> eats!i -> putsdown!i!((i+1)%N) ->
  putsdown!i!i -> getsup!i -> PHIL(i)

assert PHIL(0) :[deadlock free [F]]

Powerful User Interface

FDR4 includes a full interactive prompt that allows expressions to be evaluated, new definitions given and new assertions defined. It also includes a powerful debug viewer that allows counterexamples to be understood.

Massive Scalability

FDR4 includes a parallel refinement-checking engine that achieves a linear speed-up as the number of cores increase. It is able to check processes with billions of states, and is able to make efficient use of on-disk storage to complement memory.

FDR4 also includes a cluster version that achives a linear speedup as more compute nodes are added, thus allowing huge problems to be efficiently tackled.

New in FDR

Fully-Redesigned GUI

Featuring an interactive prompt, a more powerful debug viewer, and a built-in version of Probe.

Typechecker Included

FDR4's new type-checker produces clearer error messages in advance, not at runtime.

Parallel Refinement Checking

FDR3 is now able to use multiple cores to check refinement assertions, resulting in large speed ups.

Improved Performance

Typically, refinement checks running on a single core take half the time that FDR2 takes.

Optimising Compiler

FDR4's compiler is now able to compile a number of processes into more efficient forms.

Open-Source Frontend

The front-end has been open-sourced, allowing other tools to use the parser, type-checker and evaluator.