Diffblue 团队在 CAV'18 发表了工具文章,JBMC。这个工具是 CBMC 的扩展,目的是验证 JAVA Bytecode。JBMC 的步骤和 CBMC 类似,也是前端处理程序,转换程序到公式,然后公式传递给求解器。

JBMC 的验证步骤:

  1. Parse classes
  2. Convert to GOTO programs
  3. Symbolic Execution
  4. Solver

JBMC consists of a 1. frontend for parsing Java bytecode and a 2. Java operational model (JOM), which is an exact but verification-friendly model of the standard Java libraries.