Symbolic execution with abstraction

Authors: Saswat Anand Corina S Păsăreanu Willem Visser

Publish Date: 2008/12/11

Volume: 11, Issue: 1, Pages: 53-67

PDF Link

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 underapproximation 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: