Bug-finding and test case generation for java programs by symbolic execution

[摘要] ENGLISH ABSTRACT: In this dissertation we present a software tool, Artemis, that symbolically executes Java virtualmachine bytecode to find bugs and automatically generate test cases to trigger the bugs found. Symbolic execution is a technique of static software analysis that entails analysing code over symbolic inputs-essentially, classes of inputs-where each class is formulated as constraints over some input domain.The analysis then proceeds in a path-sensitive way adding the constraints resulting from a symbolic choice at a program branch to a path condition, and branching non-deterministically over the path condition. When a possibleerror state is reached, the path condition can be solved, and if soluble, value assignments retrieved to be used to generate explicit test cases in a unit testing framework. This last step enhances confidence that bugs are real, because testing is forced through normal language semantics, which could prevent certain states from being reached.We illustrate and evaluate Artemis on a number of examples with known errors, as well as on a large, complexcode base. A preliminary version of this work was successfully presentedat the SAICSIT conference held on 1–3 October 2012, in Centurion, South Africa.

[发布机构] Stellenbosch University