基于SAT的模型检验编码方法合理性的形式化
Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking
摘要：
有效的模型检验方法之一是利用SAT（或SMT）求解器的有效决策过程。在基于SAT的模型检验中，系统及其属性被编码成一组逻辑公式，并基于公式的可满足性来检验系统的安全性。随着编码方法的改进和制作（例如，k-induction和IC 3/PDR），验证它们的正确性变得更加重要。本研究旨在利用Coq证明助手对SMC方法进行形式化验证。我们的贡献是双重的：（1）我们将Coq中的基本编码方法、k-归纳法和IC 3/PDR（的简化版本）指定为一组简单的模块化编码谓词。(2)我们提供了一个正式的证明的合理性的编码方法的基础上，我们的形式化引理的状态序列和路径。
英文摘要：
One of the effective model checking methods is to utilize the efficient decision procedure of SAT (or SMT) solvers. In a SAT-based model checking, a system and its property are encoded into a set of logic formulas and the safety is checked based on the satisfiability of the formulas. As the encoding methods are improved and crafted (e.g., k-induction and IC3/PDR), verifying their correctness becomes more important. This research aims at a formal verification of the SMC methods using the Coq proof assistant. Our contributions are twofold: (1) We specify the basic encoding methods, k-induction and (a simplified version of) IC3/PDR in Coq as a set of simple and modular encoding predicates. (2) We provide a formal proof of the soundness of the encoding methods based on our formalized lemmas on state sequences and paths.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
