Dynamic path reduction for software model checking

We present the technique of dynamic path reduction (DPR), which allows one to prune redundant paths from the state space of a program under verification. DPR 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-thenelse 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. DPR is a very general technique which we consider here in the context of the bounded model checking of sequential programs with nondeterministic conditionals. Our preliminary experimental results show that DPR can prune a significant percentage of execution paths, a percentage that grows with the size of the instance of the problem being considered.