Modular Verification of JML Contracts Using Bounded Model Checking

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.