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).