The KEY Approach: Integrating Object-oriented Design 
                  and Formal Verification


        Authors: Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, 
	         Martin Giese, Elmar Habermalz, Reiner Hähnle, 
                 Wolfram Menzel, Peter H.Schmitt


___________________________________________________________________________


  This paper reports on the ongoing KeY project aimed at bridging
  the gap between (a) object-oriented 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.