Bounded model checking for MATLAB / Octave

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.

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

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