Object Models, Heaps, and Interpretations

paper ps   
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 language by translation into predicate calculus and interpretation of predicates in terms of objects and references in the program heap.

Citation

Viktor Kuncak and Martin Rinard. Object models, heaps, and interpretations. Technical Report 816, MIT LCS, January 2001.

BibTex Entry

@techreport{KuncakRinard01ObjectModelsHeapsInterpretations,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Object Models, Heaps, and Interpretations},
  institution = {MIT LCS},
  year = 2001,
  number = 816,
  month = {January},
  abstract = {
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 language by translation into predicate calculus and
interpretation of predicates in terms of objects and references
in the program heap.
}
}