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.