Loop Extended Symbolic Execution on List Manipulating Programs

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.130-134.3010 ◽

2011 ◽

Vol 130-134 ◽

pp. 3010-3014

Author(s):

Ren Jian Li ◽

Zhao Fei Wang ◽

Long Ming Dong

Keyword(s):

Data Structures ◽

Error Detection ◽

Symbolic Execution ◽

Quantitative Aspect ◽

Prototype Tool ◽

Recursive Data Structures ◽

Recursive Data ◽

Exit State

Current symbolic execution is challenged by its ability to deal with loops. The case gets worse for loops manipulating recursive data structures. In this paper, we extend classic symbolic execution techniques for error detection of programs manipulating lists in loops. The idea is to enhance the symbolic execution with the utilization of quantitative aspect of the shape, and to construct the exit state of the loop. The exit state is constrained by a set of numeric constraints containing normal symbolic variables in programs and instrumented symbolic variables on the shapes. A prototype tool has been implemented and experiments are conducted on some commonly used list manipulating programs.

Download Full-text

Preliminaries

10.1093/oso/9780198785156.003.0002 ◽

2017 ◽

Author(s):

David J. Lobina

Keyword(s):

Data Structures ◽

Production Systems ◽

Specific Data ◽

Recursive Functions ◽

Recursive Solution ◽

Partial Recursive Functions ◽

Recursive Structures ◽

Recursive Data Structures ◽

Recursive Data ◽

The Relationship

Recursion, or the capacity of ‘self-reference’, has played a central role within mathematical approaches to understanding the nature of computation, from the general recursive functions of Alonzo Church to the partial recursive functions of Stephen C. Kleene and the production systems of Emil Post. Recursion has also played a significant role in the analysis and running of certain computational processes within computer science (viz., those with self-calls and deferred operations). Yet the relationship between the mathematical and computer versions of recursion is subtle and intricate. A recursively specified algorithm, for example, may well proceed iteratively if time and space constraints permit; but the nature of specific data structures—viz., recursive data structures—will also return a recursive solution as the most optimal process. In other words, the correspondence between recursive structures and recursive processes is not automatic; it needs to be demonstrated on a case-by-case basis.

Download Full-text