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

JavaScript must be enabled in order to use the default MoCHi interface. To use another interface which does not require JavaScript, move to http://www.kb.ecei.tohoku.ac.jp/~ryosuke/mochi/without_js.html.

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

Hint:

1. You can use a random integer:

read_int () :: int

2. Up-to-date implementation does not support polymorphic type.