Symbolic execution is a powerful technique used to perform various activities such as program testing, formal verification of programs, etc. However, symbolic execution does not deal with indexed variables in an adequate manner. Integration of indexed variables such as arrays into symbolic execution would increase the generality of this technique. We present an original substitution technique that produces array-term-free constraints as a counterargument to the commonly accepted belief that symbolic execution cannot handle arrays. The substitution technique deals with constraints involving array terms with a single aggregate name, array terms with multiple aggregate names, and nested array terms. Our approach to solving constraints involving array terms is based on the analysis of the relationship between the array subscripts. Dataflow dependence analysis of programs involving indexed variables suffers from problems of undecidability. We propose a separation technique in which the array subscript constraints are separated from the loop path constraints. The separation technique suggests that the problem of establishing data dependencies is not as hard as the general loop problem. In this respect, we present a new general heuristic program analysis technique which is used to preserve the properties of the relations between program variables.
| Identifer | oai:union.ndltd.org:pdx.edu/oai:pdxscholar.library.pdx.edu:open_access_etds-5759 |
| Date | 06 August 1993 |
| Creators | Nikolik, Borislav |
| Publisher | PDXScholar |
| Source Sets | Portland State University |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Dissertations and Theses |
Page generated in 0.002 seconds