The Java programming language has been extended by several new concepts and constructs in release 5. In this thesis, I have brought together with KeY four of these features, examining their implications on the verification tool. The thesis comprises the analysis of enumerated types, enhanced for loops, autoboxing, and generics.

This thesis has been awarded the Förderpreis des ObjektForums 2007:

The members of the ObjektForum Karlsruhe, andrena objects ag and Technologiepark Karlsruhe, intend to honour, promote and present to the public diploma theses that have oustandingly addressed a topic in the field of software technology. (translated from German)

@misc{Ulbrich07,
  author        = {Mattias Ulbrich},
  title         = {Software Verification for {Java 5}},
  howpublished  = {Diplomarbeit, Fakult{\"a}t f{\"u}r Informatik, Universit{\"a}t Karlsruhe},
  year          = {2007}
}