Proof Reuse

Buchkapitel

Autor(en):Vladimir Klebanov
In:Verification of Object-Oriented Software: The KeY Approach
Verleger:Springer-Verlag
Reihe:LNCS 4334
Teil:III: Using the KeY System
Kapitel:13
Jahr:2007
Seiten:499-520
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.
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.
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.

BibTeX

@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.}
}