Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
surveys:mc [2010/02/16 09:47] maysam.yabandeh |
surveys:mc [2010/02/16 11:54] maysam.yabandeh |
||
|---|---|---|---|
| Line 56: | Line 56: | ||
| Not all the branches in the state graph that is obtained by symbolic execution are valid; some branches can be impossible to be traversed in a real run. The property checking module can help to prune some impossible branches. It can be used to evaluate the condition in the instruction; if the condition is evaluated as false, then the corresponding branch will be pruned, and vice versa. In Figure {{:surveys:se-statespace.gif?100|}}, the grayed branches are pruned from exploration. Consequently, the size of the space graph can be potentially much smaller than the case with early binding. | Not all the branches in the state graph that is obtained by symbolic execution are valid; some branches can be impossible to be traversed in a real run. The property checking module can help to prune some impossible branches. It can be used to evaluate the condition in the instruction; if the condition is evaluated as false, then the corresponding branch will be pruned, and vice versa. In Figure {{:surveys:se-statespace.gif?100|}}, the grayed branches are pruned from exploration. Consequently, the size of the space graph can be potentially much smaller than the case with early binding. | ||
| - | The disadvantage of symbolic execution is that the complexity is pushed to the property checking module. However, there are well-known off-the-shelf SAT solvers, which take the history of operations performed on the symbolic variable as well as the list of assumed conditions and return weather the condition is satisfiable or not. The problem is that computation time of SAT solvers is not bounded, and it can take forever for a SAT solver to response. Besides, the size of the assumed condition set and the sequence of performed operations could become too large to be efficiently handled by state-of-the-art SAT solvers. For these reasons, Symbolic Execution can also quickly stick in the state explosion problem. | + | The disadvantage of symbolic execution is that the complexity is pushed to the property checking module. However, there are well-known off-the-shelf SAT solvers, which take the history of operations performed on the symbolic variable as well as the list of assumed conditions and return whether the condition is satisfiable or not. The problem is that computation time of SAT solvers is not bounded, and it can take forever for a SAT solver to respond. Besides, the size of the assumed condition set and the sequence of performed operations could become too large to be efficiently handled by state-of-the-art SAT solvers. For these reasons, Symbolic Execution can also quickly get stuck with the state explosion problem. |
| ==== Modeling Environment ==== | ==== Modeling Environment ==== | ||