Towards a Notion of Coverage for Incomplete Program-Correctness Proofs

摘要

Deductive program verification can give high assurances for program correctness. But incomplete partial proofs do not provide any information els to what degree or with what probability the program is correct. In this paper, we introduce the concept of state space coverage for partial proofs, which estimates to what degree the proof covers the state space and the possible inputs of the program. Thus, similar to testing, the degree of assurance grows with the effort invested in constructing a correctness proof. The concept brings together deductive verification techniques with runtime techniques used to empirically estimate the coverage. We have implemented a prototypical tool that uses test data to estimate the coverage of partial proofs constructed with the program verification system KeY.