On-the-Fly Cone-of-Influence Reduction for Model Checking Concurrent Software
摘要
Calculating successor states in SMT-based software model checking is a costly task that often requires solving an SMT problem. However, in many cases, the evaluation of a program statement has no effect with respect to the verified property. Successor state calculation can be simplified in such cases. Several algorithms exist such as the cone-of-influence reduction that statically analyze the model and eliminate irrelevant variables from the model. In concurrent software, however, it is common for the result of a statement to be used in one interleaving of threads while unused in another. Algorithms that statically analyze the model cannot simplify such statements. Our on-the-fly approach detects whether a statement can be simplified during the state space exploration based on the current state of each process. Evaluation results show that our algorithm can simplify around 20% of all statements on average over a large set of benchmark programs while reducing the time of successor state calculation by more than 30% on average.