Skip to content
MoCHi: Model Checker for Higher-Order Programs
OCaml Makefile C Standard ML M4 Dockerfile
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
csisat
fpat
m4
.gitignore
.merlin
BRA_state.ml
BRA_transform.ml
BRA_transform.mli
BRA_types.ml
BRA_util.ml
CEGAR.ml
CEGAR_CPS.ml
CEGAR_CPS.mli
CEGAR_abst.ml
CEGAR_abst.mli
CEGAR_abst_CPS.ml
CEGAR_abst_CPS.mli
CEGAR_abst_util.ml
CEGAR_abst_util.mli
CEGAR_const.ml
CEGAR_fair_non_term.ml
CEGAR_lexer.mll
CEGAR_lift.ml
CEGAR_lift.mli
CEGAR_non_term.ml
CEGAR_parser.mly
CEGAR_print.ml
CEGAR_print.mli
CEGAR_ref_type.ml
CEGAR_syntax.ml
CEGAR_trans.ml
CEGAR_trans.mli
CEGAR_type.ml
CEGAR_util.ml
CEGAR_util.mli
CFA.ml
CHC.ml
CPS.ml
CPS.mli
DONE
Dockerfile
HORS_lexer.mll
HORS_parser.mly
HORS_syntax.ml
Makefile
Makefile.config.in
ModelCheck.ml
QE.ml
README.md
aclocal.m4
build
cmd.ml
color.ml
color.mli
comp_tree.ml
configure.ac
curry.ml
curry.mli
debug.ml
effect.ml
elim_same_arg.ml
encode.ml
encode.mli
encode_list.ml
encode_list.mli
encode_rec.ml
encode_rec.mli
encode_rec_variant.ml
eval.ml
extraClsDepth.ml
extraParamInfer.ml
fair_termination.ml
fair_termination_type.mli
fair_termination_util.ml
feasibility.ml
feasibility.mli
flag.ml
fpatInterface.ml
fpatInterface.mli
graph.ml
graph.mli
horSat2Interface.ml
horSat2_lexer.mll
horSat2_parser.mly
horSatInterface.ml
horSatPInterface.ml
horSat_lexer.mll
horSat_parser.mly
horSat_syntax.ml
horn_clause.ml
id.ml
inter_type.ml
lift.ml
lift.mli
main_loop.ml
mconfig.ml.in
menv.ml
mochi.fish
mochi.ml
mochi_util.ml
modular.ml
modular_check.ml
modular_common.ml
modular_common.mli
modular_infer.ml
omegaInterface.ml
parser_wrapper_4.03.ml
parser_wrapper_4.04.ml
parser_wrapper_4.05.ml
parser_wrapper_4.06.ml
parser_wrapper_4.07.ml
parser_wrapper_4.08.ml
preprocess.ml
print.ml
print.mli
problem.ml
quick_check.ml
rec_CHC_solver.ml
ref_trans.ml
ref_trans.mli
ref_type.ml
ref_type.mli
ref_type_check.ml
ref_type_check.mli
ref_type_gen.ml
ref_type_gen.mli
ref_type_pred_typing.ml
ref_type_pred_typing.mli
refine.ml
refine.mli
ret_fun.ml
rose_tree.ml
rose_tree.mli
sexp.ml
slice.ml
slice.mli
smtlib2_interface.ml
spec.ml
spec_lexer.mll
spec_parser.mly
syntax.ml
syntax.mli
term_util.ml
term_util.mli
termination_loop.ml
trans.ml
trans.mli
trans_problem.ml
trecsInterface.ml
trecs_lexer.mll
trecs_parser.mly
trecs_syntax.ml
tree.ml
tree.mli
tupling.ml
tupling.mli
type.ml
type.mli
type_check.ml
type_decl.ml
type_trans.ml
typing.ml
uncurry.ml
useless_elim.ml
util.ml
verify_module.ml
verify_ref_typ.ml
writeAnnot.ml

README.md

How to build MoCHi

Install the required tools/libraries listed below, and run "bash build", which generates "mochi.opt".

What do you need?

  • OCaml compiler (from 4.03 to 4.08)
  • Libraries available via OPAM
    • ocamlfind/findlib
    • Z3 4.7.1
    • ppx_deriving
    • Yojson
    • batteries
    • camlp4
    • camlp5
    • zarith
    • apron
  • HorSat2 binary (https://github.com/hopv/horsat2)

Dockerfile

There is a Dockerfile for compiling MoCHi. Dockerfile assumes the HorSat2 binary is in the same directory.

Licenses

This software is licensed under the Apache License, Version2.0 (http://www.apache.org/licenses/LICENSE-2.0.txt).

The software uses the following libraries/tools. Please also confirm each license of the library/tool.

Author

MoCHi is developed/maintained by Ryosuke SATO sato@ait.kyushu-u.ac.jp

Contributors

  • Hiroshi Unno
  • Takuya Kuwahara
  • Keiichi Watanabe
  • Naoki Iwayama
You can’t perform that action at this time.