An Interaction Concept for Program Verification Systems with
Explicit Proof Object
Bernhard Beckert, Sarah Grebing, Mattias Ulbrich
Deductive program verification is a difficult task: in general, user guidance
is required to control the proof search and construction. Providing the right
guiding information is challenging for users and usually requires several
reiterations. Supporting the user in this process can considerably reduce the
effort of program verification.
In this paper, we present an interaction concept for deductive program
verification systems that combines point-and-click interaction with the use of
a proof scripting language. Our contribution is twofold: Firstly, we present
a concept for a flexible and concise proof scripting language tailored to the
needs of program verification. Secondly, we explore the correspondences
between program debugging and proof debugging and introduce a concept for
analysing failed proof attempts which leverages well-established concepts from
software debugging. We illustrate our concepts on examples - including small
Java programs with non-trivial specifications - using an early prototype
implementation of our interaction concepts that is built on top of the program
verification system KeY.