Reusing Proofs when Program Verification Systems are Modified
Bernhard Beckert, Thorsten Bormer, and Vladimir Klebanov
In this position paper, we describe ongoing work on reusing deductive
proofs for program correctness when the verification system itself is
modified (including its logic, its calculus, and its proof
construction mechanism).
We build upon a method for reusing proofs when the program to be
verified is changed, which has been implemented within the KeY program
verification system and is successfully applied to reuse correctness
proofs for Java programs.