MISS_HIT 0.9.31-dev Bounded Model Checker
MISS_HIT includes a BMC tool (mh_bmc).
Gear icon

Bounded model checking for MATLAB / Octave

Work In Progress

This tool is extremely limited and incomplete. It is not going to work correctly (e.g. it will consider any variable a signed integer), if it works at all (almost all language constructs are not supported). As such this documentation is more academic in nature, and should not be considered a user manual yet.
This tool is planned to translate programs written in MATLAB or Octave to a GOTO symbol table, and then using the cbmc tool from the CPROVER tool-chain, and the CVC4 SMT Solver to perform analysis. The results will then be picked up by mh_bmc and translated back to the original MATLAB or Octave source code.
Related work:
  • gnat2goto which does the same thing, but for Ada.

Requirements

MH BMC has the following additional requirements:
  • It only works on Linux right now
  • It requires the following tools from CPROVER on your PATH
    • cbmc
    • symtab2gb
    • goto-instrument

Limitations

Currently almost nothing works, and many sweeping assumptions are made:
  • Everything is considered a 32-bit signed integer
  • Nothing beyond a tiny set of operations work
  • Only functions returning exactly one value work