KIT | KIT-Bibliothek | Impressum | Datenschutz

Generating Bounded Counterexamples for KeY Proof Obligations

Herda, Mihai

KeY is an interactive software verification system which can verify Java programs specified with JML. It uses a sequent calculus for a dynamic logic for Java. KeY supports automation to a certain degree, but when user interaction is required it is difficult to determine whether a proof obligation is invalid. For this reason, we designed and implemented a tool for finding counterexamples for KeY proof obligations. It works by translating the negation of a KeY proof obligation to an SMT specification, with all SMT sorts bounded, thus ensuring decidability. This translation is then handed over to an SMT solver. We make sure that interpreted KeY functions and predicates, preserve their semantics in order to avoid spurious counterexamples caused by the loss of their semantics. We also preserve the KeY type hierarchy. Additionally we make sure that integer over ows are not used in the found counterexamples. Because the output of the SMT solver is difficult to read, we extract the relevant information from it and present it in a user friendly manner. We have evaluated our tool on both faulty and fault free specified Java programs, and showed how the tool can be used to understand why a proof obligation is not valid.

Volltext §
DOI: 10.5445/IR/1000055929
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2014
Sprache Englisch
Identifikator urn:nbn:de:swb:90-559292
KITopen-ID: 1000055929
Verlag Karlsruher Institut für Technologie (KIT)
Umfang XIII, 112 S.
Art der Arbeit Abschlussarbeit - Master
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page