The Key System: Integrating Object-Oriented Design and Formal Methods
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Peter H. Schmitt · Lecture notes in computer science · 2002
This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1 , 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. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.