Proof Reuse for Deductive Program Verification Bernhard Beckert and Vladimir Klebanov We present a proof reuse mechanism that is based on a similarity measure for the points (formulas, terms, programs) where a rule is applied. This mechanism is particularly well-suited for program verification calculi and other calculi with (1) a large number of different rules and (2) the property that the "right" rule application can be locally identified with a high success rate, i.e., without considering the context of the current proof goal. Our method has been successfully implemented within the KeY system to reuse correctness proofs for Java programs.