Proof Reuse

@incollection{Klebanov07,
   author        = {Vladimir Klebanov},
   title         = {Proof Reuse},
   chapter       = {13},
   part          = {III: Using the {\KeY} System},
   pages         = {499--520},
   editor        = {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   booktitle     = {Verification of Object-Oriented Software: The {\KeY} Approach},
   year          = {2007}, 
   series        = {LNCS 4334},
   publisher     = {Springer-Verlag},
   doi           = {10.1007/978-3-540-69061-0_13},
   abstract      = {Experience shows that the prevalent use case of program
                    verification systems is not a single prover run. It is far
                    more likely that a proof attempt fails, and that the
                    program (and/or the specification) has to be revised. Then,
                    after a small change, it is better to adapt and reuse the
                    existing partial proof than to verify the program again
                    from first principles. A particular advantage is that proo
                    reuse can reduce the number of required user interactions.
                    \newline
                    Here we present such a technique for proof reuse. In fact,
                    towards the end of this chapter (⇒ Sect. 13.9), we will
                    show how our method can improve the user experience for
                    a whole range of verification scenarios. Until then, we
                    limit ourselves to the setting described above, with the
                    further assumption that only the implementation changes
                    and the specification remains unchanged.
                    \newline
                    After discussing the features of the method, we will
                    introduce a small running example, cover the theoretical
                    and practical details of proof reuse, examine other
                    solutions to the problem, and finally survey the full
                    range of proof reuse applications in deductive
                    verification of Java software.}
}