Loop Extended Symbolic Execution on List Manipulating Programs

Ren Jian Li; Zhao Fei Wang; Long Ming Dong

doi:10.4028/www.scientific.net/AMM.130-134.3010

Paper Titles

A 2D Numerical Model for Simulation of Two-Dimensional Circular Dam-Break
p.2993

An Improved Timing Recovery Algorithm Design
p.2997

The Analysis of the Associated Legendre Functions with Non-Integral Degree
p.3001

A Hardware Accelerate Simulator for Network Processor Based on FPGA
p.3006

Loop Extended Symbolic Execution on List Manipulating Programs
p.3010

Fault Diagnosis of Micro-Grid Based on Advanced Petri Net
p.3015

Augmented Dickey-Fuller Test and the Lag Length Selection Problem
p.3019

Generalized Polar Decompositions in Matrix Exponential
p.3023

Application of Parallel Computation in Numerical Simulation of Laser Propulsion
p.3027

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 130-134Loop Extended Symbolic Execution on List...

Loop Extended Symbolic Execution on List Manipulating Programs

Abstract:

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.

You might also be interested in these eBooks

Mechanical and Electronics Engineering III

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 130-134)

Pages:

3010-3014

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.130-134.3010

Citation:

Cite this paper

Online since:

October 2011

Authors:

Ren Jian Li, Zhao Fei Wang, Long Ming Dong

Keywords:

List Manipulating Programs, Loop Handling, Symbolic Execution

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] J. C. King, Symbolic execution and program testing, Commun. ACM, vol. 19, no. 7, p.385–394, (1976).

DOI: 10.1145/360248.360252

Google Scholar

[2] C. Cadar, D. Dunbar, and D. R. Engler, Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs, in OSDI 2008, p.209–224.

Google Scholar

[3] P. Saxena, P. Poosankam, S. Mccamant, and D. Song, Loop-extended symbolic execution on binary programs, in ISSTA (2009).

DOI: 10.21236/ada538843

Google Scholar

[4] R. Rugina, Shape analysis quantitative shape analysis, in SAS2004, p.228–245.

Google Scholar

[5] S. Gulwani, S. Jain, and E. Koskinen, Control-flow refinement and progress invariants for bound analysis, in PLDI2009, p.375–385.

DOI: 10.1145/1543135.1542518

Google Scholar

[6] A. Bouajjani, C. Dragoi, C. Enea, A. Rezine, and M. Sighireanu, Invariant synthesis for programs manipulating lists with unbounded data, in CAV2010, p.72–88.

DOI: 10.1007/978-3-642-14295-6_8

Google Scholar

[7] A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, On interprocedural analysis of programs with lists and data, in PLDI2011.

Google Scholar

[8] S. Magill, M. -H. Tsai, P. Lee, and Y. -K. Tsay, Automatic numeric abstractions for heap-manipulating programs, in POPL2010, p.211–222.

DOI: 10.1145/1707801.1706326

Google Scholar

[9] S. Magill, M. Tsai, P. Lee, and Y. Tsay, Thor: A tool for reasoning about shape and arithmetic, in CAV2008, p.428–432.

DOI: 10.1007/978-3-540-70545-1_41

Google Scholar