KIT | KIT-Bibliothek | Impressum | Datenschutz

Modular Verification of JML Contracts Using Bounded Model Checking

Klamroth, Jonas

Abstract:
In this thesis, we present an approach that allows the verification of Java programs with regard to JML annotations with a bounded model checker. We therefore translate a given Java program and its specification into a program using assumptions, assertions and nondeterministic values. The translation is proven correct for a while language and formalized for a subset of Java and JML. Additionally, a tool is presented that implements that approach and we show that the tool is capable of finding proofs in multiple case studies.

Open Access Logo


Volltext §
DOI: 10.5445/IR/1000122228
Veröffentlicht am 29.07.2020
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Hochschulschrift
Publikationsdatum 03.03.2019
Sprache Englisch
Identifikator KITopen-ID: 1000122228
Verlag KIT, Karlsruhe
Umfang iX, 62 S.
Art der Arbeit Abschlussarbeit - Master
Prüfungsdaten 03.03.2019
Referent/Betreuer Prof. Dr. Bernhard Beckert
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page