The KeY Approach:
Integrating Object Oriented Design and Formal Verification

Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese,
Elmar Habermalz, Reiner Haehnle, Wolfram Menzel, Peter H. Schmitt

This paper reports on the ongoing KeY project aimed at bridging the
gap between (a) OO software engineering methods and tools and
(b) deductive verification. A distinctive feature of our approach is
the use of a commercial CASE tool enhanced with functionality for
formal specification and deductive verification.