SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking

TL;DR

This paper presents a novel decomposition and caching scheme for SMT queries in semi-symbolic model checking, significantly improving performance by simplifying queries and reducing solver calls.

Contribution

It introduces a new symbolic state decomposition method and an efficient caching scheme, enhancing semi-symbolic model checkers' performance.

Findings

Performance gains demonstrated on Software Verification Competition benchmarks.

Reduced SMT solver calls through query simplification and caching.

Significant improvement in verification efficiency for large state spaces.

Abstract

In semi-symbolic (control-explicit data-symbolic) model checking the state-space explosion problem is fought by representing sets of states by first-order formulas over the bit-vector theory. In this model checking approach, most of the verification time is spent in an SMT solver on deciding satisfiability of quantified queries, which represent equality of symbolic states. In this paper, we introduce a new scheme for decomposition of symbolic states, which can be used to significantly improve the performance of any semi-symbolic model checker. Using the decomposition, a model checker can issue much simpler and smaller queries to the solver when compared to the original case. Some SMT calls may be even avoided completely, as the satisfaction of some of the simplified formulas can be decided syntactically. Moreover, the decomposition allows for an efficient caching scheme for quantified formulas. To support our theoretical contribution, we show the performance gain of our model checker SymDIVINE on a set of examples from the Software Verification Competition.