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.