Just test what you cannot verify!

Abstract

Today, software verification is an established analysis method which can provide high guarantees for software safety. However, the resources (time and/or memory) for an exhaustive verification are not always available, and analysis then has to resort to other techniques, like testing. Most often, the already achieved partial verification results are discarded in this case, and testing has to start from scratch. In this paper, we propose a method for combining verification and testing in which testing only needs to check the residual fraction of an uncompleted verification. To this end, the partial results of a verification run are used to construct a residual program (and residual assertions to be checked on it). The residual program can afterwards be fed into standard testing tools. The proposed technique is sound modulo the soundness of the testing procedure. Experimental results show that this combined usage of verification and testing can significantly reduce the effort for the subsequent testing.