Treffer: A Type-Theoretic Memory Model for Verification of Sequential Java Programs
Title:
A Type-Theoretic Memory Model for Verification of Sequential Java Programs
Authors:
Contributors:
The Pennsylvania State University CiteSeerX Archives
Publication Year:
1999
Collection:
CiteSeerX
Subject Terms:
Document Type:
Fachzeitschrift
text
File Description:
application/postscript
Language:
English
Relation:
Availability:
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.3E672ABD
Database:
BASE
Weitere Informationen
This paper explains the details of the memory model underlying the verification of sequential Java programs in the framework of the "LOOP" project ([13,18]). The building blocks of this memory are cells, which are untyped in the sense that they can store the contents of the fields of an arbitrary Java object. The main memory is then modeled as three infinite series of such cells, for storing instance variables on a heap, local variables and parameters on a stack, and static (or class) variables in the third series. Verification on the basis of this memory model is illustrated both in PVS and in Isabelle/HOL, via several examples of Java programs, involving various subtleties of the language (wrt. memory storage).