论文标题
形式化基于SAT的模型检查编码方法的健全性
Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking
论文作者
论文摘要
有效的模型检查方法之一是利用SAT（或SMT）求解器的有效决策过程。在基于SAT的模型检查中，将系统及其属性编码为一组逻辑公式，并根据公式的满意度检查安全性。随着编码方法得到改进和制作（例如K诱导和IC3/PDR），验证其正确性变得更加重要。这项研究旨在使用COQ证明助手对SMC方法进行正式验证。我们的贡献是双重的：（1）我们指定COQ中IC3/PDR的基本编码方法，K诱导和（简化版本）作为一组简单和模块化的编码谓词。 （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.
