MoCHi: Model Checker for Higher-Order Programs

(Termination mode)

Termination verification by MoCHi is available in this page. The algorithm is based on binary reachability analysis and inference of linear ranking functions.
For details, see Kuwahara, Terauchi, Unno and Kobayashi. "Automatic Termination Verification for Higher-Order Functional Programs" that is extended version of the paper published in ESOP 2014 (The final publication is available at

MoCHi is a software model checker for a subset of OCaml. MoCHi is based on higher-order model checking, predicate abstraction, and CEGAR (see Kobayashi, Sato and Unno. "Predicate Abstraction and CEGAR for Higher-Order Model Checking" published in PLDI 2011 for details).


1. You may use the following functions that return random values. Random.bool and
Random.bool () returns true or false non-deterministically. n(n > 0) returns a random integer between 0 and n. 0 is assumed to return an arbitrary, unbounded integer (including a negative one).
2. The current implementation does not support polymorphic types.