Date of Award

6-19-2014

Document Type

Thesis

Degree Name

Master of Science

Department

Department of Electrical and Computer Engineering

First Advisor

Gilbert L. Peterson, PhD.

Abstract

Symbolic execution is a promising technique to discover software vulnerabilities and improve the quality of code. However, symbolic execution suffers 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.

AFIT Designator

AFIT-ENG-T-14-J-3

DTIC Accession Number

ADA602534

Download

Share

COinS