Skip to main content Skip to main navigation

Publication

Analogical Transfer of Verification Proofs for State-Based Specifications

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

Abstract

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.