Publication

Analogical Transfer of Verification Proofs for State-Based Specifications

Erica Melis, Claus Sengler

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

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

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