A Metric for Testing Program Verification Systems
Bernhard Beckert, Thorsten Bormer, and Markus Wagner
The correctness of program verifiation systems is of great importance,
and it needs to be checked and demonstrated to users and certifiation
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 to judge the quality of existing
test suites for verification systems. We evaluate this coverage
criterion at two verication tools using the test suites provided by
each tool.