The KeY Platform for Verification and Analysis of Java Programs

@InProceedings{AhrendtBeckertBrunsEtAl14,
  author        = {Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns
                   and Richard Bubel and Christoph Gladisch and Sarah Grebing
                   and Reiner H\"{a}hnle and Martin Hentschel and Mihai Herda
                   and Vladimir Klebanov and Wojciech Mostowski
                   and Christoph Scheben and Peter H. Schmitt and Mattias Ulbrich},
  title         = {The {\KeY} Platform for Verification and Analysis of
                   {Java} Programs},
  year          = 2014,
  month         = oct,
  booktitle     = {6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014)},
  language      = {english},
  editor        = {Dimitra Giannakopoulou and Daniel Kroening},
  pages         = {55--71},
  publisher     = {Springer-Verlag},
  volume        = {8471},
  series        = {Lecture Notes in Computer Science},
  isbn          = {978-3-642-54107-0},
  doi           = {10.1007/978-3-319-12154-3_4},
  url           = {http://link.springer.com/chapter/10.1007/978-3-319-12154-3_4},
  abstract      = {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.}
}