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

TL;DR

This paper formalizes and verifies the soundness of encoding methods like k-induction and IC3/PDR used in SAT-based model checking using the Coq proof assistant, ensuring their correctness.

Contribution

It provides a formal specification and proof of soundness for key encoding methods in SAT-based model checking within Coq.

Findings

Formal specifications of k-induction and IC3/PDR in Coq

Soundness proofs for encoding methods

Enhanced confidence in model checking correctness

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.