Symbolic execution with abstraction |
| |
Authors: | Saswat Anand Corina S P?s?reanu Willem Visser |
| |
Affiliation: | (1) College of Computing, Georgia Institute of Technology, Atlanta, GA, USA;(2) NASA Ames Research Center, Moffett Field, Mountain View, CA 94035, USA;(3) SEVEN Networks, Redwood City, CA, USA |
| |
Abstract: | We address the problem of error detection for programs that take recursive data structures and arrays as input. Previously
we proposed a combination of symbolic execution and model checking for the analysis of such programs: we put a bound on the size of the program inputs and/or the search depth of the model checker to limit the search state space. Here we look
beyond bounded model checking and consider state matching techniques to limit the state space. We describe a method for examining
whether a symbolic state that arises during symbolic execution is subsumed by another symbolic state. Since the number of symbolic states may be infinite, subsumption is not enough to ensure termination.
Therefore, we also consider abstraction techniques for computing and storing abstract states during symbolic execution. Subsumption
checking determines whether an abstract state is being revisited, in which case the model checker backtracks—this enables
analysis of an under-approximation of the program behaviors. We illustrate the technique with abstractions for lists and arrays. We also discuss abstractions
for more general data structures. The abstractions encode both the shape of the program heap and the constraints on numeric
data. We have implemented the techniques in the Java PathFinder tool and we show their effectiveness on Java programs. This
paper is an extended version of Anand et al. (Proceedings of SPIN, pp. 163–181, 2006). |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|