Analogical Transfer of Verification Proofs for State-Based Specifications

Erica Melis, Claus Sengler

DFKI DFKI Research Reports (RR) 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.

RR-97-01.pdf (pdf, 203 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence