Analogical Transfer of Verification Proofs for State-Based Specifications

The amount of user interaction is the prime cause of costs in interactive program verification. This paper describes an internal analogy technique that reuses subproofs in the verification of state-based specifications. It identifies common patterns of subproofs and their justifications in order reuse these subproofs; thus significant savings on the number of user interactions in a verification proof are achievable. 1 Introduction Software verification is the job of taming complexity: in order to verify, say one hundred thousand lines of source code, several ten thousands of proof obligations have to be shown, some of which may require formal proofs of up to eight or ten thousand steps. Usually these long proofs consist of a considerable number of relatively simple subproofs to be established. Even for a small percentage of interactive steps, i.e., those steps the user has to supply as opposed to those steps that are generated automatically by the system (in the VSE system [3] curre..