Generating Bounded Counterexamples for KeY Proof Obligations

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.