符号执行和模型检查(例如在模型转换中)之间的区别是什么?我不明白它们的区别。他们是一样的吗?
在模型检查中，您必须将系统编码为有限状态机，并将该FSM提供给模型检查器以及规范。然后，模型检查器将确保规范始终保持在该系统中。
在符号执行中，您只提供您的程序，符号执行引擎将检查所有可行的路径来生成测试输入或检查断言。
一个简单的例子来说明它们的区别:并发性。模型检查可以处理多线程系统，因为它在FSM中被指定为输入，然而，符号执行不能处理多个线程。模型检验:一种正式验证程序是否满足规范的方法。该规范通常以时间逻辑公式的形式给出，如:"如果输入是x，输出必须是y -对于程序的所有执行(全局)保持"(参见例如Edward a Lee)。
符号模型检查与显式状态检查:程序可以是有限状态机(FSM)。这里显式的状态检查就足够了。但幸运的是，模型检查器也适用于扩展的FSM、并发的、概率的、实时的应用程序。为了防止那些具有非常大(无限)数量状态的系统中的状态爆炸，使用了符号模型检查。在符号模型中，检查状态和输入等被视为符号和命题公式(或状态集、集合操作等)。为了执行模型检查，需要进行可达性分析，为此，程序转换被象征性地执行。这些检查器不能使用插装本机代码的正常执行。
符号执行:在符号执行过程中存在不同的编码方法。有些非常特定于模型检查，有些是模块化的，并用于独立的符号执行框架，因为它是由符号执行的发明者定义的。符号执行框架通常还使用符号模型检查的一些元素(探索，搜索)来用于测试等。
最后一些例子:
JPF, java - pathfinder:模型检查器，显式状态检查，输入:java字节码
SPF，符号寻径器:符号执行，扩展JPFJCBMC: Bounded Model Checker，扩展了JPF, SPF
XRTs:探索和符号执行，输入:CIL字节码
IntelliTest:参数化单元测试使用XRTs
Spec Explorer:基于模型的测试使用XRTs