问实现不需要模型检查的符号执行

EN

你需要：

• 用于符号化执行的语言的解析器，可以构建ASTs。
• 名称解析(以及相关的符号表)，因此当执行引擎遇到标识符时，它可以确定关联的类型和值。
• 控制流分析，使符号执行引擎能够通过程序跟踪控制流。
• 一种符号代数，可以合成和简化符号术语。这需要一个解析器(所以你可以输入这样的方程)和打印机(这样你就可以看到它计算的内容)。
• 在符号执行开始点指定假定值的方法

这是相当多的机械，很难在一个地方找到它。很难只为一个工具来构建它，这也是你找不到这么多工具的原因之一。

我们的DMS软件重组工具包有所有的必要条件。你可能会发现用DMS实现符号语言的一个例子很有趣。