SMT/SAT 求解器与模型检查器答案

【问题标题】：SMT/SAT Solver vs Model CheckerSMT/SAT 求解器与模型检查器
【发布时间】：2017-05-11 07:16:32
【问题描述】：

最近，我开始研究形式验证技术。在文献中，model checker 和 solver 在某种程度上可以互换使用。但是，模型检查器和求解器如何相互连接？

附言如果建议一些论文或链接，我将不胜感激。

【问题讨论】：

【解决方案1】：

在模型检查中，您有一个模型和一个规范（或属性），然后您检查模型是否符合规范。

在 SAT 解题中，您有一个公式，然后您尝试为它找到一个令人满意的作业。

现在，在模型检查中，您可以结合模型和属性的否定来给您一个公式。使用求解器求解此公式。如果它为您提供了解决方案，则意味着该属性有时会受到侵犯（因为您结合了否定属性）。获得unsat 意味着您的模型满足属性/规范。

【讨论】：

【解决方案2】：

要执行模型检查，需要进行可达性分析，为此，程序转换通常以符号方式执行。由此产生的满意度问题的解决方案由求解器创建。在这本免费教科书（第三部分：分析和验证）中有一个非常基本且非常好的介绍：

Edward A. Lee 和 Sanjit A. Seshia，嵌入式系统简介，网络物理系统方法，第二版，麻省理工学院出版社，ISBN 978-0-262-53381-2，2017 年

【讨论】：