Shape analysis with reference set relations

Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Scopus citations


Tracking subset relations between the contents containers on the heap is fundamental to modeling the semantics of many common programing idioms such as applying a function to a subset of objects and maintaining multiple views of the same set of objects. We introduce a relation, must reference sets, which subsumes the concept of must-aliasing and enables existing shape analysis techniques to efficiently and accurately model many types of containment properties without the use of explicit quantification or specialized logics for containers/sets. We extend an existing shape analysis to model the concept of reference sets. Reference sets allow the analysis to efficiently track a number of important relations (must-=, and must-⊆) between objects that are the targets of sets of references (variables or pointers). We show that shape analysis augmented with reference set information is able to precisely model sharing for a range of data structures in real programs that cannot be expressed using simple must-alias information. In contrast to more expressive proposals based on logic languages (e.g., extensions of first-order predicate logic with transitive closure or the use of a decision procedure for sets), reference sets can be efficiently tracked in a shape analyzer.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings
Number of pages16
StatePublished - 2010
Event11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010 - Madrid, Spain
Duration: Jan 17 2010Jan 19 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5944 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Shape analysis with reference set relations'. Together they form a unique fingerprint.

Cite this