KIT | KIT-Bibliothek | Impressum | Datenschutz

Modular Verification of JML Contracts Using Bounded Model Checking

Beckert, Bernhard ORCID iD icon; Kirsten, Michael ORCID iD icon; Klamroth, Jonas; Ulbrich, Mattias ORCID iD icon


There are two paradigms for dealing with complex verification targets: Modularization using contract-based specifications and whole-program analysis. In this paper, we present an approach bridging the gap between the two paradigms, introducing concepts from the world of contract-based deductive verification into the domain of software bounded model checking. We present a transformation that takes Java programs annotated with contracts written in the Java Modeling Language and turns them into Java programs that can be read by the bounded model checker JBMC. A central idea of the translation is to make use of nondeterministic value assignments to eliminate JML quantifiers. We have implemented our approach and discuss an evaluation, which shows the advantages of the presented approach.

Postprint §
DOI: 10.5445/IR/1000125411
Veröffentlicht am 30.10.2021
DOI: 10.1007/978-3-030-61362-4_4
Zitationen: 5
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2020
Sprache Englisch
Identifikator ISBN: 978-3-030-61361-7
ISSN: 1611-3349
KITopen-ID: 1000125411
Erschienen in ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium (ISoLA 2020)
Verlag Springer
Seiten 60–80
Serie Lecture Notes in Computer Science ; 12476
Projektinformation KASTEL_SKI (BMBF, EU 6. RP, 16KIS0843)
Vorab online veröffentlicht am 29.10.2020
Schlagwörter Software verification, Modular design, Design by contract, Software bounded model checking
Nachgewiesen in Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page