A metric for testing program verification systems

Abstract

The correctness of program verification systems is of great importance, and it needs to be checked and demonstrated to users and certification agencies. One of the contributing factors to the correctness of the whole verification system is the correctness of the background axiomatization, respectively the correctness of calculus rules. In this paper, we examine how testing verification systems is able to provide evidence for the correctness of the rule base or the axiomatization. For this, we present a new coverage criterion called axiomatization coverage, which allows us to judge the quality of existing test suites for verification systems. We evaluate this coverage criterion at two verification tools using the test suites provided by each tool.