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 link.springer.com).
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).
Random.bool and Random.int.Random.bool () returns true or false non-deterministically.Random.int n(n > 0) returns a random integer between 0 and n.Random.int 0 is assumed to return an arbitrary, unbounded integer (including a negative one).