Symcretic testing of programs

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

Dinges, Peter

关键词: Software Testing;    Concolic Execution;    Backward Execution;    Goal-Directed;    Heuristic Search;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/72743/Peter_Dinges.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

Targeted inputs are input values for a program that lead to theexecution of a user-specified branch or statement.Targeted inputsare useful: In debugging, for example, they allow programmers tofollow the execution towards the program point where a bug occurred.In testing, they constitute a test case that covers a new piece ofcode.A natural approach to find targeted inputs is symbolic backwardexecution.However, symbolic backward execution struggles withcomplicated arithmetic, external method calls, and data-dependentloops that occur in many real-world programs.This dissertation describes symcretic execution, a novel method forefficiently finding targeted inputs.Symcretic execution overcomesthe limitations of symbolic backward execution by integrating it withconcrete forward execution.The approach consists of two phases: Inits first phase, symcretic execution uses symbolic backward executionto find a feasible execution path from the given target to any of theprogram's entry points.Unlike prior approaches, symcretic executionskips over constraints that are problematic for the symbolic decisionprocedure and defers their solution until the second phase.Thesecond phase of symcretic execution begins when the symbolic executionreaches an entry point.In this phase, symcretic execution usesconcrete forward execution and heuristic search to find inputs thatsatisfy the constraints that were skipped in the first phase.Acomparison with related approaches and an empirical evaluation suggestthat symcretic execution finds more inputs that result in relevantexecutions while avoiding the exploration of uninteresting paths.The heuristic search algorithm employed in the second phase ofsymcretic execution must be able to handle complicated arithmetic andexternal method calls.The dissertation therefore introduces analgorithm called concolic walk.The concolic walk algorithm alsoapplies to solving path conditions in customary symbolic and concolicexecution and is thus presented in this more general setting.Theconcolic walk algorithm is a heuristic search based on a geometricinterpretation of the task of finding inputs.An evaluation of thealgorithm shows that it finds more solutions (and hence improvescoverage) than the simplification-based heuristics that have been usedin concolic testing.Moreover, the concolic walk algorithm improvesthe effectiveness of state-of-the-art concolic test generators thatare using powerful specialized constraint solvers.