Combining static analysis and constraint solving for automatic test case generation

Date of this Version


Document Type

Conference Paper

Publication Details

Citation only

Vorobyov, K., & Krishnan, P. (2012). Combining static analysis and constraint solving for automatic test case generation. Paper presented at the 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (ICST), 17-21 April. Montreal, QC, Canada

Access the conference

2012 HERDC submission. FoR code: 080309

© Copyright IEEE, 2012




We present an approach in automatic test generation that combines features of static analysis and bounded symbolic computation that is capable of producing a test suite that can be used to declare a program under test safe within bounds. We first use the results produced by static analysis which will identify a list of potential errors in the program. We restrict our search to the locations where errors can exist and aim to find exactly one test case per real bug. We have built a prototype tool (called Batg) that implements our approach. We report the results of running it on a number of benchmarks from well known benchmarking suites. We compare Batgto KLEE (an automatic test generation framework) and CBMC(a bounded model checker). This comparison is based on the time taken by the tools, the number of bugs found and the number of generated test cases. We analyse the results of our experiment, demonstrating the benefits of our approach.

This document is currently not available here.



This document has been peer reviewed.