The KeY Tool
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin
Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas
Roth, Steffen Schlager, and Peter H. Schmitt
KeY is a tool that provides facilities for formal specification and
verification of programs within a commercial platform for UML based
software development. Using the KeY Tool, formal methods and
object-oriented development techniques are applied in an integrated
manner. Formal specification is performed using the Object Constraint
Language (OCL), which is part of the UML standard. KeY provides support
for the authoring and formal analysis of OCL constraints. The target
language of KeY based development is Java Card, a proper subset of Java
for smart card applications and embedded systems. KeY uses a dynamic
logic for Java Card to express proof obligations, and provides a
state-of-the-art theorem prover for interactive and automated
verification. Apart from its integration into UML based software
development, a characteristic feature of KeY is that formal
specification and verification can be introduced incrementally.