Slicing Execution with Partial Weakest Precondition for Model Abstraction of C Programs
Model abstraction plays an important role in model checking of source codes of programs. Slicing execution is a lightweight symbolic execution procedure to extract the models of C programs in an over-approximated way. In this paper, we present an approach to improving slicing execution with a novel concept called partial weakest precondition (PWP) to alleviate the space explosion problem. PWPs specify the corresponding weakest precondition conservatively by only considering part of program variables. We present how to integrate PWP with slicing execution, which leads to a compact model with much smaller state space compared with the one obtained by the original slicing execution. A new PWP implementation is also presented to avoid possible exponential PWP formula size and support pointers and aliases as well. The distinguished features of the implementation are that it does not need to translate the program to the passive form beforehand, and it supports loops very well. Comparing with slicing execution without PWP, the experimentation on SSL protocol based on the C source code openssl-0.9.6c shows that the state space may be reduced to only 1/10 after applying PWP.