Sciweavers

Share
IFM
2009
Springer

Dynamic Path Reduction for Software Model Checking

10 years 6 months ago
Dynamic Path Reduction for Software Model Checking
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 π 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 π 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 π 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 ...
Zijiang Yang, Bashar Al-Rawi, Karem Sakallah, Xiao
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where IFM
Authors Zijiang Yang, Bashar Al-Rawi, Karem Sakallah, Xiaowan Huang, Scott A. Smolka, Radu Grosu
Comments (0)
books