The KeY Platform for Verification and Analysis of Java Programs

Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch,
Sarah Grebing, Reiner H\"{a}hnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov,
Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich


The KeY system offers a platform of software analysis tools for sequential Java.
Foremost, this includes full functional verification against contracts written
in the Java Modeling Language. But the approach is general enough to provide a
basis for other methods and purposes: (i) complementary validation techniques
to formal verification such as testing and debugging, (ii) methods that reduce
the complexity of verification such as modularization and abstract
interpretation, (iii) analyses of non-functional properties such as information
flow security, and (iv) sound program transformation and code generation. We
show that deductive technology that has been developed for full functional
verification can be used as a basis and framework for other purposes than pure
functional verification. We use the current release of the KeY system as an
example to explain and prove this claim.