KIT | KIT-Bibliothek | Impressum | Datenschutz

Proving Well-Definedness of JML Specifications with KeY

Kirsten, Michael

Abstract:
Specification methods in formal program verification enable the enhancement of source code with formal annotations as to formally specify the behaviour of a program. This is a popular way in order to subsequently prove software to be
reliable and meet certain requirements, which is crucial for many applications and gains even more importance in modern society. The annotations can be taken as a contract, which then can be verified guaranteeing the specified program element – as a receiver – to fulfil this contract with its caller. However, these functional contracts ca ... mehr

Abstract (englisch):
Specification methods in formal program verification enable the enhancement of source code with formal annotations as to formally specify the behaviour of a program. This is a popular way in order to subsequently prove software to be reliable and meet certain requirements, which is crucial for many applications and gains even more importance in modern society. The annotations can be taken as a contract, which then can be verified guaranteeing the specified program element – as a receiver – to fulfil this contract with its caller. However, these functional contracts can ... mehr

Open Access Logo


Volltext §
DOI: 10.5445/IR/1000092717
Veröffentlicht am 28.03.2019
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Jahr 2013
Sprache Englisch
Identifikator urn:nbn:de:swb:90-927170
KITopen-ID: 1000092717
Verlag KIT, Karlsruhe
Umfang 77 S.
Abschlussart Abschlussarbeit - Bachelor
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page