The KeY Platform for Verification and Analysis of Java Programs

Reviewed Paper In Proceedings

Author(s):Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich
In:6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014)
Publisher:Springer-Verlag
Series:Lecture Notes in Computer Science
Volume:8471
Year:2014
Pages:1-17
URL:http://link.springer.com/chapter/10.1007/978-3-319-12154-3_4
DOI: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.

BibTeX

@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        = {Giannakopoulou, Dimitra and Kroening, Daniel},
  pages         = {1--17},
  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.}
}