solver - SMT/SAT解算器与模型检查器

Question

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

p.s.如果建议提供一些论文或链接，我将不胜感激。

Answer 1

为了执行模型检查，需要进行可达性分析，并且为此，通常需要象征性地执行程序转换。由求解器创建对所得满意度问题的解决方案。这本免费教科书中有一个非常基础且非常好的介绍(第三部分:分析和验证):

http://leeseshia.org

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