sha*_*b0z 5 model-checking solver smt sat
最近，我开始研究形式验证技术。在文献中，模型检查器和求解器以某种方式互换使用。但是，模型检查器和求解器是如何相互连接的？
ps 如果建议一些论文或链接，我将不胜感激。
在模型检查中，您有一个模型和一个规范（或属性），然后检查模型是否满足规范。
在 SAT 求解中，你有一个公式，然后你尝试为其找到令人满意的作业。
现在，在模型检查中，您可以将模型与属性的否定结合起来，得到一个公式。使用求解器求解该公式。如果它为您提供了解决方案，则意味着有时会违反该属性（因为您连接了否定的属性）。获得unsat意味着您的模型满足属性/规格。
为了执行模型检查，需要进行可达性分析，为此，程序转换通常以符号方式执行。由此产生的满意度问题的解决方案是由求解器创建的。在这本免费教科书中可以找到非常基本且非常好的介绍（第三部分：分析和验证）：
Edward A. Lee 和 Sanjit A. Seshia，嵌入式系统简介，网络物理系统方法，第二版，麻省理工学院出版社，ISBN 978-0-262-53381-2，2017 年