Skip to main content Skip to main navigation


Analogical Transfer of Verification Proofs for State-Based Specifications

Erica Melis; Claus Sengler
DFKI, DFKI Research Reports (RR), Vol. 97-01, 1/1997.


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.