@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.} }
The KeY Platform for Verification and Analysis of Java Programs
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: | 55-71 |
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.