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
Hrsg.: Giannakopoulou, Dimitra ; Kroening, Daniel (2014)
The KeY Platform for Verification and Analysis of Java Programs.
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2014 |
| Herausgeber: | Giannakopoulou, Dimitra ; Kroening, Daniel |
| Autor(en): | 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 |
| Art des Eintrags: | Bibliographie |
| Titel: | The KeY Platform for Verification and Analysis of Java Programs |
| Sprache: | Deutsch |
| Publikationsjahr: | Juli 2014 |
| Verlag: | Springer |
| Buchtitel: | Post-Conference Proceedings VSTTE 2014 |
| Reihe: | LNCS |
| Kurzbeschreibung (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. |
| ID-Nummer: | TUD-CS-2014-0832 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik > Software Engineering 20 Fachbereich Informatik |
| Hinterlegungsdatum: | 31 Dez 2016 10:40 |
| Letzte Änderung: | 16 Mai 2018 12:06 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum