Verification of Java Programs with Generics

Several proof systems allow the formal verification of Java programs, and a specification language was specifically designed for Java. However, none of these systems support generics that were introduced in Java 5. Generics are very important and useful when the collection framework (lists, sets, hash tables etc.) is used. Though they are mainly dealt with at compile time, they have some effect on the run time behavior of a Java program. Most notably, heap pollution can cause exceptions. A verification system for Java must incorporate these effects. In this paper we describe what effects can occur at run time, and how they are handled in the KIV system. To the authors knowledge, this makes KIV the first verification system to support generics.