Constraint Reusing and k-Induction for Three-Valued Bounded Model Checking

Abstract

Refinement-based model checking is an approach to software verification: Starting with an abstract software model, the model is iteratively refined until it is precise enough to prove or refute the property of interest. A downside is that it typically takes several iterations until the necessary precision is reached, and thus, resources are spent on repeating work that has already been performed in previous iterations. We tackle this by introducing a concept for reusing information between refinement iterations in order to reduce the computational overhead. Our approach extends our previous work on three-valued abstraction (3VA) and bounded model checking (BMC). 3VA allows to translate a verification problem into a SAT-encoded three-valued BMC problem that can be checked via a SAT solver. While there was formerly no information sharing between refinement iterations, we now show that logic constraints learned by the solver in the current iteration are also valid in future iterations. Reusing such constraints enables to prune the search space of SAT which leads to a speed-up of the iterative approach. Since we previously used standard BMC, the technique was incomplete and could be only used for detecting property violations but not for proving their absence. Here we combine three-valued BMC with k-induction, which makes the approach complete for model checking safety properties.