User-Defined Backtracking Criteria for Symbolic Execution

Scott Kausler, Elena Sherman

Research output: Contribution to journalArticlepeer-review

Abstract

Symbolic execution is a path-sensitive program analysis technique that aids users with program verification. To avoid exploring infeasible paths, symbolic execution checks the prefix of a current path for feasibility by adding a branch constraint to the path prefix and passing the formula to an off-the-shelf SMT solver for an evaluation. If the solver returns SAT/UNSAT, then the prefix is marked as feasible/infeasible.

However, the solver can also return an UNKNOWN result, which means it cannot evaluate the formula. In addition, an operation occurring before a constraint can cause over-approximation that propagates to the solver's result. Moreover, symbolic execution might time out the solver if it takes too long to run. A symbolic execution tool might handle these uncertainties by backtracking or by continuing its exploration of the prefix.

This paper examines the behavior of path constraints beyond uncertain backtracking points. String and integer constraints are collected from concrete program execution via dynamic symbolic execution. These constraints are used to analyze how over- approximation in a path prefix affects the completeness of its extensions. We also examine variations in time required to decide a path constraint. Our findings suggest that a custom backtracking criteria defined by the user does improve the completeness of symbolic execution.

Original languageAmerican English
JournalComputer Science Faculty Publications and Presentations
DOIs
StatePublished - 1 Jan 2014

Keywords

  • constraint analysis
  • constraint solving
  • symbolic execution

EGS Disciplines

  • Computer Sciences

Fingerprint

Dive into the research topics of 'User-Defined Backtracking Criteria for Symbolic Execution'. Together they form a unique fingerprint.

Cite this