2026-09-19T07:09:55Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/72743 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Heuristic Search Symcretic testing of programs Agha, Gul A. Agha, Gul A. Adve, Vikram S. Dig, Danny Sirjani, Marjan Dinges, Peter 2015-01-21T19:47:36Z 2015-01-21T19:47:36Z 2014-12 2015-01-21 2014-12 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. Item withdrawn by Laura Spradlin (lspradl2@illinois.edu) on 2014-11-26T17:21:17Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Dinges_Peter.pdf: 907439 bytes, checksum: 47ff1c4b70f50e4661dea3f99e5f76b6 (MD5) Made available in DSpace on 2015-01-21T19:47:36Z (GMT). No. of bitstreams: 1 Peter_Dinges.pdf: 907439 bytes, checksum: 47ff1c4b70f50e4661dea3f99e5f76b6 (MD5) http://hdl.handle.net/2142/72743 en Copyright 2014 Peter Dinges Software Testing Concolic Execution Backward Execution Goal-Directed text Computer Science 1434 Computer Science 0112 University of Illinois at Urbana-Champaign Dissertation Ph.D. PHD:Computer Science -UIUC 10KS0112PHD