在没有模型检查的情况下实现符号执行答案

【问题标题】：implement symbolic execution without model-checking在没有模型检查的情况下实现符号执行
【发布时间】：2016-09-14 12:34:48
【问题描述】：

如何在不使用model checking 和Finite State Machine (FSM)（例如not，例如Java Path Finder）的情况下为particular language 实现symbolic execution？我需要有关它的详细信息。例如，我可以通过什么语言来实现这个符号执行以及我需要知道哪些其他事情？

【问题讨论】：

标签： testing verification model-checking symbolic-execution

【解决方案1】：

你需要：

可以构建 AST 的符号执行语言的解析器
名称解析（和关联的符号表），因此当您的执行引擎遇到标识符时，它可以确定关联的类型和值
控制流分析，使符号执行引擎可以通过程序跟踪控制流
一种可以组合和简化符号项的符号代数。这需要一个解析器（这样你就可以输入这样的方程）和漂亮的打印机（这样你就可以看到它计算了什么）
一种在符号执行开始时指定假定值的方法

这是相当多的机器，很难在一个地方找到它们。只为一个工具构建它更难，这也是你找不到很多这样的工具的部分原因。

我们的DMS Software Reengineering Toolkit 具备所有条件。你可能会觉得an example of a symbolic language implemented with DMS很有趣。

【讨论】：

感谢您的帮助。如果我想使用模型检查上述步骤会发生什么变化？使用模型检查是否比不使用时更容易实现符号执行？
对于模型检查，您必须愿意为每个状态枚举不同的符号模拟，并对不允许的状态添加约束。因为状态空间很大，你可能希望所有这些都并行。 DMS 具有并行基础：-} 见semanticdesigns.com/Products/DMS/ParlanseForDMS.html
非常感谢。请您再解释一下答案的第四项和第五项？
第 4 项：参见链接“用 DMS 实现的符号语言”。特别是，这意味着能够构建代数/布尔公式，并使用代数定律机械地/自动地简化这些公式。第 5 项：您需要选择代码的一部分，并指定该代码开始执行的（代数）条件（“前提条件”）。
非常感谢。