Modular Verification of JML Contracts Using Bounded Model Checking

@mastersThesis{KlamrothMSc2019,
  author   = {Jonas Klamroth},
  title    = {Modular Verification of {JML} Contracts
              Using Bounded Model Checking},
  school   = {Karlsruhe Institute of Technology},
  month    = mar,
  year     = {2019},
  language = {english},
  doi      = {10.5445/IR/1000122228},
  abstract = {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.},
  location = {Karlsruhe, Germany}
}