## Symbolic heap

We assume a fixed finite set \textsf{Vars} of program variables (ranged over by $x,y, ...$) and an infinite set \textsf{Lvars} of logical variables (ranged over by $x',y',...$)

Definition : A symbolic heap $\Pi| \Sigma$ consists of a finite set $\Pi$ of equalities and a finite set $\Sigma$ of heap predicates. The equalities $E =F$ are between expressions $E$ and $F$, which are variables $x$, or primed variables $x'$, or \textrm{nil}. The elements of $\Sigma$ are of the form

E\mapsto F, \textrm{ls}(E,F), \textrm{junk}

The points-to assertion $E\mapsto F$ can hold only in a singleton heap, where $E$ is the only active cell. Similarly, when a list segment \textrm{ls}(E,F) holds of a given heap, the path it traces out is unique, and goes through all cells in the heap.

For each symbolic heap $\Pi| \Sigma$, the $\Pi$ is called pure part of $\Pi| \Sigma$, and $\Sigma$ spatial part of $\Pi| \Sigma$.

The \textrm{junk} predicate is used in the canonicalization phase to swallow up garbage.

\textsf{Values} = \textsf{Locations} \cup \{ \textsf{nil}\},

h \in \textsf{Heaps} = \textsf{Locations} \rightharpoonup_f \textsf{Values},
s \in \textsf{Stacks} = (\textsf{Vars} \cup \textsf{Lvars}) \rightarrow \textsf{Values},

\textsf{States} = \textsf{Stacks} \times \textsf{Heaps}

## Static analysis

### Trend one: the abstract domain uses formulae from the logic

For example, to do program analysis for linked list programs, the abstract domain uses formulae from separation logic. The partial order of abstract values is denoted by entailment of formulae. That is, if $\phi \Rightarrow \psi$ ($\phi$ entails $\psi$), then $v_{\phi} \sqsubseteq v_{\psi}$ (where $v_{\phi}$ and $v_{\psi}$ are two abstract values represented by formula $\phi$ and $\psi$).