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 |
Options (only for editors)
![]() |
Show editorial Details |