Using State Merging and State Pruning to Address the Path Explosion Problem Faced by Symbolic Execution

Abstract

Symbolic execution is a promising technique to discover software vulnerabilities and improve the quality of code. However, symbolic execution su ers from a path explosion problem where the number of possible paths within a program grows exponentially with respect to loops and conditionals. New techniques are needed to address the path explosion problem. This research presents a novel algorithm which combines the previously researched techniques of state merging and state pruning. A prototype of the algorithm along with a pure state merging and pure state pruning are implemented in the KLEE symbolic execution tool with the goal of increasing the code coverage. Each algorithm is tested over 66 of the GNU COREUTILS utilities. State merging combined with state pruning outperforms the unmodified version of KLEE on 53% of the COREUTILS. These results confirm that state merging with pruning has viability in addressing the path explosion problem of symbolic execution.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 19, 2014
Accession Number
ADA602534

Entities

People

  • Patrick T. Copeland

Organizations

  • Air Force Institute of Technology

Tags

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Computer Programs
  • Computers
  • Debugging
  • Department Of Defense
  • Engineering
  • Experimental Design
  • Governments
  • Information Operations
  • Instructions
  • Operating Systems
  • Software Testing
  • Test And Evaluation
  • Test Methods
  • Trees (Data Structures)
  • United States

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.