The KeY System: Integrating Object-Oriented Design and Formal Methods
Wolfgang Ahrendt
Thomas Baar
Bernhard Beckert
Martin Giese
Reiner Hähnle
Wolfram Menzel
Wojciech Mostowski
Peter H. Schmitt
This paper gives a brief description of the KeY system, a tool
written as part of the ongoing KeY project, which is aimed at
bridging the gap between (a) OO software engineering methods and
tools and (b) deductive verification. The KeY system consists of a
commercial CASE tool enhanced with functionality for formal
specification and deductive verification.