MoCHi: Model Checker for Higher-Order Programs

MoCHi is a software model checker for a subset of OCaml programming language. MoCHi is based on higher-order model checking, predicate abstraction, and CEGAR (see this paper for details). This page provides a web interface to an extension of MoCHi for a relatively complete verification, which is described in the following paper:
Automating Relatively Complete Verification of Higher-Order Functional Programs
Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi
Accepted for publication in POPL 2013.
[short version PDF] [full version PDF]
The benchmark programs can be downloaded as a single zip file from here.

Enter an OCaml program in the box below, and press the "verify" button.