[ list |
abstracts |
bib ]

## Existential Heap Abstraction Entailment is Undecidable

paper pdf
paper ps
### Abstract

In this paper we study constraints for specifying properties
of data structures consisting of linked objects allocated in
the heap. Motivated by heap summary graphs in role analysis
and shape analysis we introduce the notion of *regular
graph constraints*.
A regular graph constraint is a graph representing the heap
summary; a heap satisfies a constraint if and only if the
heap can be homomorphically mapped to the summary. Regular
graph constraints form a very simple and natural fragment of
the existential monadic second-order logic over graphs.
One of the key problems in a compositional static analysis
is proving that procedure preconditions are satisfied
at every call site. For role analysis, precondition
checking requires determining the validity of implication,
i.e., *entailment* of regular graph constraints.
The central result of this paper is the undecidability of
regular graph constraint entailment. The
*undecidability* of the *entailment* problem is
surprising because of the simplicity of regular graph
constraints: in particular, the *satisfiability* of
regular graph constraints is *decidable*.
Our undecidability result implies that there is no complete
algorithm for statically checking procedure preconditions or
postconditions, simplifying static analysis results, or
checking that given analysis results are correct. While
incomplete conservative algorithms for regular graph
constraint entailment checking are possible, we argue that
heap specification languages should avoid second-order
existential quantification in favor of explicitly specifying
a criterion for summarizing objects.

### Citation

Viktor Kuncak and Martin Rinard.
Existential heap abstraction entailment is undecidable.
In *10th Annual International Static Analysis Symposium*, volume
2694 of *LNCS*, San Diego, California, June 11-13 2003.### BibTex Entry

@INPROCEEDINGS{KuncakRinard03ExistentialHeapAbstractionEntailment,
author = {Viktor Kuncak and Martin Rinard},
title = {Existential Heap Abstraction Entailment is Undecidable},
booktitle = {10th Annual International Static Analysis Symposium},
year = 2003,
address = {San Diego, California},
month = {June 11-13},
series = {LNCS},
volume = {2694},
localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03ExistentialHeapAbstractionEntailment.pdf}
}

[ list |
abstracts |
bib ]