Deductive Software Verification - The KeY Book:
From Theory to Practice
Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle,
Peter H. Schmitt, and Mattias Ulbrich (eds.)
The ultimate goal of program verification is not the theory behind the tools
or the tools themselves, but the application of the theory and tools in the
software engineering process. Our society relies on the correctness of a vast
and growing amount of software. Improving the software engineering process is
an important, long-term goal with many steps. Two of those steps are the KeY
tool and this KeY book.
The material is presented on an advanced level suitable for graduate courses
and, of course, active researchers with an interest in verification. The
underlying verification paradigm is deductive verification in an expressive
program logic. The logic used for reasoning about programs is not a minimalist
version suitable for theoretical investigations, but an industrial-strength
version. The first-order part is equipped with a type system for modelling of
object hierarchies, with underspecification, and with various built-in
theories. The program logic covers full Java Card (plus a bit more such as
multi-dimensional arrays, characters, and long integers). A lot of emphasis is
thereby put on specification, including two widely-used object-oriented
specification languages (OCL and JML) and even an interface to natural
language generation. The generation of proof obligations from specified code
is discussed at length. The book is rounded off by two substantial case
studies that are included and presented in detail.