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 ax-iomatization, 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 sys-tems. We evaluate this coverage criterion at two verification tools using the test suites provided by each tool.