Verification of Memory Performance Contracts with KeY
Abstract:
Determining the worst case memory consumption is an important
issue for real-time Java applications. This work describes a
methodology for formally verifying worst case memory performance
constraints and proposes extensions to Java Modeling Language
(JML) facilitating better verifiability of JML performance
specifications.
issue for real-time Java applications. This work describes a
methodology for formally verifying worst case memory performance
constraints and proposes extensions to Java Modeling Language
(JML) facilitating better verifiability of JML performance
specifications.
| Zugehörige Institution(en) am KIT | Institut für Theoretische Informatik (ITI) |
| Publikationstyp | Forschungsbericht/Preprint |
| Publikationsjahr | 2007 |
| Sprache | Englisch |
| Identifikator | ISSN: 1432-7864 urn:nbn:de:swb:90-68082 KITopen-ID: 1000006808 |
| Verlag | Universität Karlsruhe (TH) |
| Serie | Interner Bericht. Fakultät für Informatik, Universität Karlsruhe ; 2007,8 |