Show simple item record

dc.contributor.advisorFoster, Jeffrey Sen_US
dc.contributor.advisorHicks, Michaelen_US
dc.contributor.authorMa, Kin Keungen_US
dc.date.accessioned2012-02-17T07:14:29Z
dc.date.available2012-02-17T07:14:29Z
dc.date.issued2011en_US
dc.identifier.urihttp://hdl.handle.net/1903/12399
dc.description.abstractSymbolic execution is an automated technique for program testing that has recently become practical, thanks to advances in constraint solvers. Generally speak- ing, a symbolic executor interprets a program with symbolic inputs, systematically enumerating execution paths induced by the symbolic inputs and the program's control flow. In this dissertation, I discuss the architecture and implementation of Otter, a symbolic execution framework for C programs, and work that uses Otter to solve two program analysis problems. Firstly, we use Otter to solve the line reachability problem--given a line target in a program, find inputs that drive the program to the line. We propose two new directed search strategies, one using a distance metric to guide symbolic execution towards the target, and another iteratively running symbolic execution from the start of the function containing the target, then jumping backward up the call chain to the start of the program. We compare variants of these strategies with several existing undirected strategies from the literature on a suite of 9 GNU Coreutils programs. We find that most directed strategies perform extremely well in many cases, although they sometimes fail badly. However, by combining the distance metric with a random-path strategy, we obtain a strategy that performs best on average over our benchmarks. We also generalize the line reachability problem to multiple line targets, and evaluate our new strategies under a different experimental setup. The result shows that many directed strategies start off slightly slower than undirected strategies, but they catch up and perform the best in the long run. Another use of Otter is to study how run-time configuration options affect the behavior of configurable software systems. We conjecture that, at certain levels of abstraction, software configuration spaces are much smaller than combinatorics might suggest. To evaluate our conjecture, we ran Otter on three configurable software systems with their concrete test suites, but making configuration options symbolic. Otter generated data of all execution paths of these systems, from which we discovered how the settings of configuration options affect line, basic block, edge, and condition coverage for our subjects under the test suites. Had we instead run the test suites under all configuration settings, it would have required many orders of magnitude more executions to generate the same data.en_US
dc.titleImproving Program Testing and Understanding via Symbolic Executionen_US
dc.typeDissertationen_US
dc.contributor.publisherDigital Repository at the University of Marylanden_US
dc.contributor.publisherUniversity of Maryland (College Park, Md.)en_US
dc.contributor.departmentComputer Scienceen_US
dc.subject.pqcontrolledComputer scienceen_US
dc.subject.pquncontrolledprogramming languagesen_US
dc.subject.pquncontrolledprogram testingen_US
dc.subject.pquncontrolledstatic analysisen_US
dc.subject.pquncontrolledsymbolic executionen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record