System testing and program verification

Abstract

The effectiveness of black-box system testing can be increased by automatic program verification techniques. For example, the redundancy of a test case can be detected by static analysis; the analysis must be applied to a program in the `whitebox' layer of the system under test (e.g., in the setting of GUI testing, to the program which defines the event handlers). We will investigate the question of how automatic program verification techniques can be used to reduce the cost of testing and at the same time provide a guarantee for test coverage.