Incremental Proofs for Bounded Model Checking

Abstract

Bounded model checkers show the validity of a property of a hardware or software system to hold up to a certain bound by solving a sequence of related Boolean satisfiability (SAT) problems. An incremental SAT solver, a tool often used by such model checkers, can exploit similarities between these consecutive SAT problems. By avoiding repeated work incremental solving is much more efficient. To increase the trustworthiness of a model checker, it is however important to provide assurance about the correctness of its underlying solving engine. Though modern SAT solvers are expected to produce an independently verifiable certificate when a formula is unsatisfiable, incremental SAT solving involves multiple formulae under different temporary assumptions. In this paper we propose a new proof format for SAT solvers applicable to incremental use cases and demonstrate the viability of it in the context of bounded hardware model checking.