MISS_HIT includes a BMC tool (mh_bmc).
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.
- gnat2goto which does the same thing, but for Ada.
MH BMC has the following additional requirements:
- It only works on Linux right now
- It requires the following tools from CPROVER on your PATH
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