We present the new technique of dynamic path reduction (DPR), which allows one to prune redundant paths from the state space of a program under verification. DPR is a very general technique which we consider here in the context of the bounded model checking of sequential programs with nondeterministic conditionals. The DPR approach is based on the symbolic analysis of concrete executions. For each explored execution path p that does not reach an abort statement, we repeatedly apply a weakest-precondition computation to accumulate the constraints associated with an infeasible sub-path derived from p, by taking the alternative branch to an if-then-else statement. We then use an SMT solver to learn the minimally unsatisfiable core of these constraints. By further learning the statements in p that are critical to the sub-path's infeasibility, as well as the control-flow decisions that must be taken to execute these statements, unexplored paths containing the same unsatisfiable core can be efficiently and dynamically pruned. Our preliminary experimental results show that DPR can prune a signicant percentage of execution paths, a percentage that grows with the size of the instance of the problem being considered.
In Proc. of iFM'09, the 7th International Conference on Integrated Formal Methods, Duesseldorf, Germany, February 2009, Springer, LNCS.
*This work was supported by the NSF Faculty Early Career Development Award CCR01-33583.