Symbolic execution with abstraction

被引：38

作者：

Anand S. ^{[1
]}

Pǎsǎreanu C.S. ^{[2
]}

Visser W. ^{[3
]}

机构：

[1] College of Computing, Georgia Institute of Technology, Atlanta, GA

[2] NASA Ames Research Center, Mountain View, CA 94035, Moffett Field

[3] SEVEN Networks, Redwood City, CA

来源：

International Journal on Software Tools for Technology Transfer | 2009年 / 11卷 / 01期

关键词：

Model Check; Array Element; Path Condition; Symbolic Execution; Symbolic State;

D O I：

10.1007/s10009-008-0090-1

中图分类号：

学科分类号：

摘要：

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). © Springer-Verlag 2008.

引用

页码：53 / 67

页数：14

共 31 条

[11]

Ghiya R., Hendren L.J., Is it a tree, a DAG, or a cyclic graph? a shape analysis for heap-directed pointers in c, Proceedings of POPL, pp. 1-15, (1996)

[12]

Godefroid P., Klarlund N., Sen K., DART: Directed automated random testing, Proceedings of PLDI, pp. 213-223, (2005)

[13]

Gopan D., DiMaio F., Dor N., Reps T., Sagiv M., Numeric domains with summarized dimensions In:, Proceedings of TACAS, pp. 512-529, (2004)

[14]

Gopan D., Reps T., Sagiv M., A framework for numeric analysis of array operations, Proceedings of POPL, pp. 338-350, (2005)

[15]

Henzinger T.A., Jhala R., Majumdar R., Sutre G., Software verification with BLAST, Proceedings of SPIN, pp. 235-239, (2003)

[16]

Holzmann G.J., Joshi R., Model-driven software verification, Proceedings of SPIN, pp. 76-91, (2004)

[17]

Java PathFinder

[18]

Khurshid S., Pasareanu C., Visser W., Generalized symbolic execution for model checking and testing, Proceedings of TACAS, pp. 553-568, (2003)

[19]

Khurshid S., Suen Y., Generalizing symbolic execution to library classes, Proceedings of PASTE, pp. 103-110, (2005)

[20]

King J.C., Symbolic execution and program testing, Commun. ACM, 19, 7, pp. 385-394, (1976)

← 1 2 3 4 →