MoCHi: Model Checker for Higher-Order Programs

MoCHi is a software model checker for a subset of OCaml. MoCHi is based on higher-order model checking, predicate abstraction, and CEGAR (see this paper for details).

The source code is available here. (The version may be different from one on this web interface.)

The example programs are available here.