TU Darmstadt / ULB / TUbiblio

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 ; Klebanov, Vladimir ; Mostowski, Wojciech ; Scheben, Christoph ; Schmitt, Peter ; Ulbrich, Mattias
Giannakopoulou, Dimitra ; Kroening, Daniel (eds.) (2014):
The KeY Platform for Verification and Analysis of Java Programs.
In: LNCS, In: Post-Conference Proceedings VSTTE 2014, pp. 55--71,
Springer, [Conference or Workshop Item]

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, methods that reduce the complexity of verification such as modularization and abstract interpretation, (ii) analyses of non-functional properties such as information flow security, and %worst-case execution time, (iii) 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.

Item Type: Conference or Workshop Item
Erschienen: 2014
Editors: Giannakopoulou, Dimitra ; Kroening, Daniel
Creators: Ahrendt, Wolfgang ; Beckert, Bernhard ; Bruns, Daniel ; Bubel, Richard ; Gladisch, Christoph ; Grebing, Sarah ; Hähnle, Reiner ; Hentschel, Martin ; Klebanov, Vladimir ; Mostowski, Wojciech ; Scheben, Christoph ; Schmitt, Peter ; Ulbrich, Mattias
Title: The KeY Platform for Verification and Analysis of Java Programs
Language: German
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, methods that reduce the complexity of verification such as modularization and abstract interpretation, (ii) analyses of non-functional properties such as information flow security, and %worst-case execution time, (iii) 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.

Book Title: Post-Conference Proceedings VSTTE 2014
Series: LNCS
Publisher: Springer
Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Date Deposited: 31 Dec 2016 10:40
Identification Number: TUD-CS-2014-0832
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)
Show editorial Details Show editorial Details