CBMC教程 (3) - GOTO programs

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

JBMC 的验证步骤：

Parse classes
Convert to GOTO programs
Symbolic Execution
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.