OCaml implementation of dynamic partial-order reduction model-checking algorithm, and accompanying dissertation.