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).
Input a program and click "verify" button.
NOTE:
The verifier will time-out for some programs that takes long time to verify.