Symcretic testing of programs

Dinges, Peter

Permalink

https://hdl.handle.net/2142/72743 Copy

Description

Title

Symcretic testing of programs

Author(s)

Dinges, Peter

Issue Date

2015-01-21

Director of Research (if dissertation) or Advisor (if thesis)

Agha, Gul A.

Doctoral Committee Chair(s)

Agha, Gul A.

Committee Member(s)

• Adve, Vikram S.
• Dig, Danny
• Sirjani, Marjan

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• Software Testing
• Concolic Execution
• Backward Execution
• Goal-Directed
• Heuristic Search

Abstract

Targeted inputs are input values for a program that lead to the execution of a user-specified branch or statement. Targeted inputs are useful: In debugging, for example, they allow programmers to follow the execution towards the program point where a bug occurred. In testing, they constitute a test case that covers a new piece of code. A natural approach to find targeted inputs is symbolic backward execution. However, symbolic backward execution struggles with complicated arithmetic, external method calls, and data-dependent loops that occur in many real-world programs. This dissertation describes symcretic execution, a novel method for efficiently finding targeted inputs. Symcretic execution overcomes the limitations of symbolic backward execution by integrating it with concrete forward execution. The approach consists of two phases: In its first phase, symcretic execution uses symbolic backward execution to find a feasible execution path from the given target to any of the program's entry points. Unlike prior approaches, symcretic execution skips over constraints that are problematic for the symbolic decision procedure and defers their solution until the second phase. The second phase of symcretic execution begins when the symbolic execution reaches an entry point. In this phase, symcretic execution uses concrete forward execution and heuristic search to find inputs that satisfy the constraints that were skipped in the first phase. A comparison with related approaches and an empirical evaluation suggest that symcretic execution finds more inputs that result in relevant executions while avoiding the exploration of uninteresting paths. The heuristic search algorithm employed in the second phase of symcretic execution must be able to handle complicated arithmetic and external method calls. The dissertation therefore introduces an algorithm called concolic walk. The concolic walk algorithm also applies to solving path conditions in customary symbolic and concolic execution and is thus presented in this more general setting. The concolic walk algorithm is a heuristic search based on a geometric interpretation of the task of finding inputs. An evaluation of the algorithm shows that it finds more solutions (and hence improves coverage) than the simplification-based heuristics that have been used in concolic testing. Moreover, the concolic walk algorithm improves the effectiveness of state-of-the-art concolic test generators that are using powerful specialized constraint solvers.

Graduation Semester

2014-12

Permalink

http://hdl.handle.net/2142/72743

Copyright and License Information

Copyright 2014 Peter Dinges

Owning Collections