Sciweavers

AMAST
2008
Springer

Verification of Java Programs with Generics

14 years 2 months ago
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 [18] [2]. To the authors knowledge, this makes KIV the first verification system to support Java's generics.
Kurt Stenzel, Holger Grandy, Wolfgang Reif
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where AMAST
Authors Kurt Stenzel, Holger Grandy, Wolfgang Reif
Comments (0)