- Java programs often use pointer structures for normal computations. A verification system for Java should have good proof support for reasoning about those structures. However, the literature for pointer verification almost always uses specifications and definitions that are tailored to the problem under consideration. We propose a generic specification for Java pointer structures that allows to express many important properties, and is easy to use in proofs. The specification is part of the Java calculus in the KIV prover.
