Unfolding Based Minimal Test Suites for Testing Multithreaded Programs

This paper focuses on the problem of computing the minimal test suite for a terminating multithreaded program that covers all its executable statements. We have in previous work shown how to use unfoldings to capture the true concurrency semantics of multithreaded programs and to generate test cases for it. In this paper we rely on this earlier work and show how the unfolding can be used to generate the minimal test suite that covers all the executable statements of the program. The problem of generating such a minimal test suite is shown to be NP-complete in the size of the unfolding, and as a side result, covering executable transitions of any terminating safe Petri net is also NP-complete in the size of its unfolding. We propose SMT-encodings to these problems and give initial results on applying this encoding to compute the minimal test suite for several benchmarks.