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.
read_int () :: int2. Up-to-date implementation does not support polymorphic type.