KIT | KIT-Bibliothek | Impressum

Generating Bounded Counterexamples for KeY Proof Obligations

Herda, Mihai

Abstract:
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 show ... mehr


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