## Existential Heap Abstraction Entailment is Undecidable

paper ps
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 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,
month = {June},
series = {LNCS},
volume = {2694},
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 \emph{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., \emph{entailment} of regular graph constraints.

The central result of this paper is the undecidability of
regular graph constraint entailment.  The
\emph{undecidability} of the \emph{entailment} problem is
surprising because of the simplicity of regular graph
constraints: in particular, the \emph{satisfiability} of
regular graph constraints is \emph{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.
}
}