Similarities and reuse of proofs in formal software verification

The amount of user interaction is a prime cost factor in interactive program verification. This paper analyzes situations in which the reuse of previous proofs can help reducing these costs. In particular, it describes a technique that reuses subproofs in the verification of invariants of state transition systems. This technique replays decisions of generalized previous proof attempts from the same overall verification process. As opposed to CBR applications that are justified by the fact that no or insufficient domain knowledge is available to solve a problem from first principles or by saving a huge search effort, our technique aims at saving user interaction. Several case studies provide first proofs of significant savings of user interaction in verification proofs by employing our CBR. technique.