MoCHi

MoCHi: Model Checker for Higher-Order Programs. MoCHi is a software model checker for a subset of OCaml. MoCHi is based on higher-order model checking, predicate abstraction, and CEGAR (see this paper for details).


References in zbMATH (referenced in 11 articles )

Showing results 1 to 11 of 11.
Sorted by year (citations)

  1. Kobayashi, Naoki; Lago, Ugo Dal; Grellois, Charles: On the termination problem for probabilistic higher-order recursive programs (2020)
  2. Asada, Kazuyuki; Kobayashi, Naoki; Sin’ya, Ryoma; Tsukada, Takeshi: Almost every simply typed (\lambda)-term has a long (\beta)-reduction sequence (2019)
  3. Kobayashi, Naoki: Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable (2019)
  4. Ong, C.-H. Luke: Automata, logic and games for the (\lambda)-calculus (2017)
  5. Sato, Ryosuke; Kobayashi, Naoki: Modular verification of higher-order functional programs (2017)
  6. Sin’ya, Ryoma; Asada, Kazuyuki; Kobayashi, Naoki; Tsukada, Takeshi: Almost every simply typed (\lambda)-term has a long (\beta)-reduction sequence (2017)
  7. Suzuki, Ryota; Fujima, Koichi; Kobayashi, Naoki; Tsukada, Takeshi: Streett automata model checking of higher-order recursion schemes (2017)
  8. Pham, Tuan-Hung; Gacek, Andrew; Whalen, Michael W.: Reasoning about algebraic data types with abstractions (2016)
  9. Terao, Taku; Tsukada, Takeshi; Kobayashi, Naoki: Higher-order model checking in direct style (2016)
  10. Yasukata, Kazuhide; Tsukada, Takeshi; Kobayashi, Naoki: Verification of higher-order concurrent programs with dynamic resource creation (2016)
  11. Kuwahara, Takuya; Sato, Ryosuke; Unno, Hiroshi; Kobayashi, Naoki: Predicate abstraction and CEGAR for disproving termination of higher-order functional programs (2015)