TU Darmstadt / ULB / TUbiblio

The KeY Platform for Verification and Analysis of Java Programs

Ahrendt, Wolfgang and Beckert, Bernhard and Bruns, Daniel and Bubel, Richard and Gladisch, Christoph and Grebing, Sarah and Hähnle, Reiner and Hentschel, Martin and Klebanov, Vladimir and Mostowski, Wojciech and Scheben, Christoph and Schmitt, Peter and Ulbrich, Mattias Giannakopoulou, Dimitra and Kroening, Daniel (eds.) (2014):
The KeY Platform for Verification and Analysis of Java Programs.
In: LNCS, In: Post-Conference Proceedings VSTTE 2014, Springer, pp. 55--71, [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 and Kroening, Daniel
Creators: Ahrendt, Wolfgang and Beckert, Bernhard and Bruns, Daniel and Bubel, Richard and Gladisch, Christoph and Grebing, Sarah and Hähnle, Reiner and Hentschel, Martin and Klebanov, Vladimir and Mostowski, Wojciech and Scheben, Christoph and Schmitt, Peter and 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.

Title of Book: Post-Conference Proceedings VSTTE 2014
Series Name: 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
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)

View Item View Item