Proof reuse for deductive program verification
Bernhard Beckert, Vladimir Klebanov · 2004
We present a proof reuse mechanism for deductive program verification calculi. It reuses proofs incrementally (one proof step at a time) and is employs a similarity measure for the points (formulas, terms, programs) where a rule is applied.