LCS Publication Details
Publication Title: Object Models, Heaps and Interpretations
Publication Author: Kuncak, Viktor
Additional Authors: Marint Rinard
LCS Document Number: MIT-LCS-TR-816
Publication Date: 1-8-2001
LCS Group: Computer Architecture
Additional URL: No URL Given
This paper explores the use of object models for specifying verifiable heap invariants. We define a simple language based on sets and relations and illustrate its use through examples. We give formal semantics of the laguage by translation into predicate calculus and interpretation of predicates in terms of objects and references in the program heap.
To obtain this publication:

To purchase a printed copy of this publication please contact MIT Document Services.