SMT/SAT 求解器与模型检查器
SMT/SAT Solver vs Model Checker
最近开始研究形式化验证技术。在文献中，model checker 和 solver 可以互换使用。
但是，模型检查器和求解器如何相互连接？
p.s。如果推荐一些论文或链接，我将不胜感激。
要执行模型检查，需要进行可达性分析，为此，程序转换通常以符号方式执行。由此产生的满意度问题的解决方案由求解器创建。在这本免费教科书（第三部分：分析与验证）中找到了一个非常基础和非常好的介绍：
Edward A. Lee 和 Sanjit A. Seshia，嵌入式系统简介，网络物理系统方法，第二版，麻省理工学院出版社，ISBN 978-0-262-53381-2，2017
在模型检查中，你有一个模型和一个规格（或属性），你检查模型是否符合规格。
在 SAT 求解中，你有一个公式，你试图找到一个令人满意的分配给它。
现在，在模型检查中，您可以结合模型和 属性 的否定来得到一个公式。使用求解器求解此公式。如果它给你一个解决方案，那就意味着 属性 有时会被违反（因为你连接了取反的 属性）。获得 unsat 意味着您的模型满足 property/specification.
最近开始研究形式化验证技术。在文献中，model checker 和 solver 可以互换使用。 但是，模型检查器和求解器如何相互连接？
p.s。如果推荐一些论文或链接，我将不胜感激。
要执行模型检查，需要进行可达性分析，为此，程序转换通常以符号方式执行。由此产生的满意度问题的解决方案由求解器创建。在这本免费教科书（第三部分：分析与验证）中找到了一个非常基础和非常好的介绍：
Edward A. Lee 和 Sanjit A. Seshia，嵌入式系统简介，网络物理系统方法，第二版，麻省理工学院出版社，ISBN 978-0-262-53381-2，2017
在模型检查中，你有一个模型和一个规格（或属性），你检查模型是否符合规格。
在 SAT 求解中，你有一个公式，你试图找到一个令人满意的分配给它。
现在，在模型检查中，您可以结合模型和 属性 的否定来得到一个公式。使用求解器求解此公式。如果它给你一个解决方案，那就意味着 属性 有时会被违反（因为你连接了取反的 属性）。获得 unsat 意味着您的模型满足 property/specification.