KeY: A Formal Method for Object-Oriented Systems
Wolfgang Ahrendt, Bernhard Beckert, Reiner Haehnle, Peter H. Schmitt
This paper gives an overview of the KeY approach and highlights the
main features of the KeY system. KeY is an approach (and a system)
for the deductive verification of object-oriented software. It aims
for integrating design, implementation, formal specification and
formal verification as seamlessly as possible. The intention is to
provide a platform that allows close collaboration of conventional and
formal software development methods.