Software Verification for Java 5

Diploma Thesis

Author(s):Mattias Ulbrich
School:Fakultät für Informatik, Universität Karlsruhe
Year:2007
URL:http://lfm.iti.kit.edu/files/theses/diploma/Software_Verf_Java5.pdf
Links:

Abstract

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.

Note

This thesis has been awarded the Förderpreis ObjektForum 2007

BibTeX

@misc{Ulbrich2007,
  author        = {Mattias Ulbrich},
  title         = {Software Verification for {Java 5}},
  howpublished  = {Diplomarbeit, Fakult{\"a}t f{\"u}r Informatik,
                  Universit{\"a}t Karlsruhe},
  school        = {Fakult{\"a}t f{\"u}r Informatik,
                  Universit{\"a}t Karlsruhe},
  type          = {Diplomarbeit},
  year          = {2007},
  abstract = {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.},
  url = {http://lfm.iti.kit.edu/files/theses/diploma/Software_Verf_Java5.pdf},
  links = {Presentation:http://lfm.iti.kit.edu/files/theses/diploma/slides_SW_Verf_Java5.pdf;
           Short presentation:http://lfm.iti.kit.edu/files/theses/diploma/KeYJava5Kurz.pdf},
  note = {This thesis has been awarded the {F{\"o}rderpreis ObjektForum 2007}}
}