The KeY platform for verification and analysis of Java programs

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; Mattias Ulbrich

doi:10.1007/978-3-319-12154-3_4

The KeY platform for verification and analysis of Java programs

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, Mattias Ulbrich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

27 Citations (Scopus)

50 Downloads (Pure)

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.

Original language	English
Title of host publication	Verified Software: Theories, Tools and Experiments
Subtitle of host publication	6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers
Editors	Dimitra Giannakopoulou, Daniel Kroening
Place of Publication	Cham
Publisher	Springer
Pages	55-71
Number of pages	17
ISBN (Electronic)	978-3-319-12154-3
ISBN (Print)	978-3-319-12153-6
DOIs	https://doi.org/10.1007/978-3-319-12154-3_4
Publication status	Published - 14 Oct 2014
Event	6th International Conference on Verified Software: Theories, Tools and Experiments, VSTTE 2014 - Vienna, Austria Duration: 17 Jul 2014 → 18 Jul 2014

Publication series

Name	Lecture Notes In Computer Science
Publisher	Springer
Volume	8471
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	6th International Conference on Verified Software: Theories, Tools and Experiments, VSTTE 2014
Period	17/07/14 → 18/07/14
Other	17-18 July 2014

Keywords

Testing
System description
Theorem proving
Java
Visualization
Verification
Security

Access to Document

10.1007/978-3-319-12154-3_4

Fingerprint Dive into the research topics of 'The KeY platform for verification and analysis of Java programs'. Together they form a unique fingerprint.

Cite this

Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., Hähnle, R., Hentschel, M., Herda, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P. H., & Ulbrich, M. (2014). The KeY platform for verification and analysis of Java programs. In D. Giannakopoulou, & D. Kroening (Eds.), Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers (pp. 55-71). (Lecture Notes In Computer Science; Vol. 8471). Springer. https://doi.org/10.1007/978-3-319-12154-3_4

Ahrendt, Wolfgang ; Beckert, Bernhard ; Bruns, Daniel ; Bubel, Richard ; Gladisch, Christoph ; Grebing, Sarah ; Hähnle, Reiner ; Hentschel, Martin ; Herda, Mihai ; Klebanov, Vladimir ; Mostowski, Wojciech ; Scheben, Christoph ; Schmitt, Peter H. ; Ulbrich, Mattias. / The KeY platform for verification and analysis of Java programs. Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. editor / Dimitra Giannakopoulou ; Daniel Kroening. Cham : Springer, 2014. pp. 55-71 (Lecture Notes In Computer Science).

@inproceedings{5f9412d3c2fd43d58d1f3a2077f2b6ec,

title = "The KeY platform for verification and analysis of Java programs",

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.",

keywords = "Testing, System description, Theorem proving, Java, Visualization, Verification, Security",

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 Schmitt, {Peter H.} and Mattias Ulbrich",

note = "eemcs-eprint-25325 ; 6th International Conference on Verified Software: Theories, Tools and Experiments, VSTTE 2014 ; Conference date: 17-07-2014 Through 18-07-2014",

year = "2014",

month = oct,

day = "14",

doi = "10.1007/978-3-319-12154-3_4",

language = "English",

isbn = "978-3-319-12153-6",

series = "Lecture Notes In Computer Science",

publisher = "Springer",

pages = "55--71",

editor = "Dimitra Giannakopoulou and Daniel Kroening",

booktitle = "Verified Software: Theories, Tools and Experiments",

}

Ahrendt, W, Beckert, B, Bruns, D, Bubel, R, Gladisch, C, Grebing, S, Hähnle, R, Hentschel, M, Herda, M, Klebanov, V, Mostowski, W, Scheben, C, Schmitt, PH & Ulbrich, M 2014, The KeY platform for verification and analysis of Java programs. in D Giannakopoulou & D Kroening (eds), Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. Lecture Notes In Computer Science, vol. 8471, Springer, Cham, pp. 55-71, 6th International Conference on Verified Software: Theories, Tools and Experiments, VSTTE 2014, 17/07/14. https://doi.org/10.1007/978-3-319-12154-3_4

The KeY platform for verification and analysis of Java programs. / Ahrendt, Wolfgang; Beckert, Bernhard; Bruns, Daniel; Bubel, Richard; Gladisch, Christoph; Grebing, Sarah; Hähnle, Reiner; Hentschel, Martin; Herda, Mihai; Klebanov, Vladimir; Mostowski, Wojciech; Scheben, Christoph; Schmitt, Peter H.; Ulbrich, Mattias.

Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. ed. / Dimitra Giannakopoulou; Daniel Kroening. Cham : Springer, 2014. p. 55-71 (Lecture Notes In Computer Science; Vol. 8471).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - The KeY platform for verification and analysis of Java programs

AU - Ahrendt, Wolfgang

AU - Beckert, Bernhard

AU - Bruns, Daniel

AU - Bubel, Richard

AU - Gladisch, Christoph

AU - Grebing, Sarah

AU - Hähnle, Reiner

AU - Hentschel, Martin

AU - Herda, Mihai

AU - Klebanov, Vladimir

AU - Mostowski, Wojciech

AU - Scheben, Christoph

AU - Schmitt, Peter H.

AU - Ulbrich, Mattias

N1 - eemcs-eprint-25325

PY - 2014/10/14

Y1 - 2014/10/14

N2 - 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.

AB - 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.

KW - Testing

KW - System description

KW - Theorem proving

KW - Java

KW - Visualization

KW - Verification

KW - Security

U2 - 10.1007/978-3-319-12154-3_4

DO - 10.1007/978-3-319-12154-3_4

M3 - Conference contribution

SN - 978-3-319-12153-6

T3 - Lecture Notes In Computer Science

SP - 55

EP - 71

BT - Verified Software: Theories, Tools and Experiments

A2 - Giannakopoulou, Dimitra

A2 - Kroening, Daniel

PB - Springer

CY - Cham

T2 - 6th International Conference on Verified Software: Theories, Tools and Experiments, VSTTE 2014

Y2 - 17 July 2014 through 18 July 2014

ER -

Ahrendt W, Beckert B, Bruns D, Bubel R, Gladisch C, Grebing S et al. The KeY platform for verification and analysis of Java programs. In Giannakopoulou D, Kroening D, editors, Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. Cham: Springer. 2014. p. 55-71. (Lecture Notes In Computer Science). https://doi.org/10.1007/978-3-319-12154-3_4