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 example programs are available here.
Input a program and click "verify" button.