Reasoning about Pointer Structures in Java

Reasoning about Pointer Structures in Java

erschienen 11.12.2006 in: Universität Augsburg, Technical Report 2006-30 Technical Report, Institute of Computer Science, University of Augsburg, December 2006

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.

Downloads:

• Reasoning about Pointer Structures in Java  -  (techreport-pointers-java.pdf, 202 KB)