MoCHi: Model Checker for Higher-Order Programs

(Non-termination mode)

(The benchmark set used in our CAV2015 paper is available here.)

Non-termination verification by MoCHi is available in this page. The method is based on predicate abstraction computing a mixture of over- and under-approximation, and CEGAR on two kinds of counterexample paths.

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).

Input a program (or select our benchmark programs from the select box), and click "verify" button.
verbose mode


1. You can use a random integer:
read_int () :: int
2. Up-to-date implementation does not support polymorphic type.