Analyzing unsatisfiability in bounded model checking using MAX-SMT and dual slicing

Abstract

Bounded model checking (BMC) with satisfiability modulo theories (SMT) is a powerful approach for generating test cases or finding bugs. However, it is generally difficult to determine an appropriate unrolling bound k in BMC. An SMT formula for BMC might be unsatisfiable because of the insufficiency of k. In this paper, we propose a novel approach for BMC using partial maximum satisfiability, in which the initial conditions of state variables are treated as soft constraints. State variables whose initial conditions are not satisfied in the solution of a maximum satisfiability solver can be regarded as bottlenecks in BMC. We can simultaneously estimate modified initial conditions for these bottleneck variables, with which the formula becomes satisfiable. Furthermore, we propose a method based on dual slicing to delineate the program path that is changed when we modify the initial conditions of the specified bottlenecks. The analysis results help us to estimate a suitable unrolling bound. We present experimental results using examples from the automotive industry to demonstrate the usefulness of the proposed method.