Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking
Abstract
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.
Cite
@article{arxiv.2006.13613,
title = {Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking},
author = {Daisuke Ishii and Saito Fujii},
journal= {arXiv preprint arXiv:2006.13613},
year = {2022}
}
Comments
Accepted to be published in the 14th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2020; path length k+1 in the bounded safety encoding, which was redundant, was decremented; fixed typo in Eq (12)