Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking

Daisuke Ishii, Saito Fujii

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 enc…