Quantified Data Automata on Skinny Trees:
an Abstract Domain for Lists
Pranav Garg1 , P. Madhusudan1 , Gennaro Parlato2

arXiv:1304.0660v1 [cs.PL] 2 Apr 2013

1

University of Illinois at Urbana-Champaign, USA
2
University of Southampton, UK

Abstract. We propose a new approach to heap analysis through an
abstract domain of automata, called automatic shapes. The abstract domain uses a particular kind of automata, called quantified data automata
on skinny trees (QSDAs), that allows to define universally quantified
properties of singly-linked lists. To ensure convergence of the abstract
fixed-point computation, we introduce a sub-class of QSDAs called elastic QSDAs, which also form an abstract domain. We evaluate our approach on several list manipulating programs and we show that the proposed domain is powerful enough to prove a large class of these programs
correct.

1

Introduction

The abstract analysis of heap structures is an important problem in program
verification as dynamically evolving heap is ubiquitous in modern programming,
either in terms of low level pointer manipulation or in object-oriented programming. Abstract analysis of the heap is hard because abstractions need to represent the heap that is of unbounded size, and must capture both the structure of
the heap as well as the unbounded data stored in the heap. While several datadomains have been investigated for data stored in static variables, the analysis
of unbounded structure and unbounded data that a heap contains has been
less satisfactory. The primary abstraction that has been investigated is the rich
work on shape analysis [29]. However, unlike abstractions for data-domains (like
intervals, octagons, polyhedra, etc.), shape analysis requires carefully chosen instrumentation predicates to be given by the user, and often are particular to
the program that is being verified. Shape analysis techniques typically merge
all nodes that satisfy the same unary predicate, achieving finiteness of the abstract domain, and interpret the other predicates using a 3-valued (must, must
not, may) abstraction. Moreover, these instrumentation predicates often require
to be encoded in particular ways (for example, capturing binary predicates as
particular kinds of unary predicates) so as to not lose precision.
For instance, consider a sorting algorithm that has an invariant of the form:
∀x, y. ( (x →∗next y ∧ y →∗next i) ⇒ d(x) ≤ d(y) )
which says that the sub-list before pointer i is sorted. In order to achieve a
shape-analysis algorithm that discovers this invariant (i.e., captures this invariant precisely during the analysis), we typically need instrumentation predicates

such as p(z) = z →∗next i, s(x) = ∀y.((x →∗next y ∧ y →∗next i) ⇒ d(x) ≤ d(y)),
etc. The predicate s(x) says that the element that is at x is less than or equal to
the data stored in every cell between x and i. These instrumentation predicates
are clearly too dependent on the precise program and property being verified.
In this paper, we investigate an abstract domain for heaps that works without
user-defined instrumentation predicates (except we require that the user fix an
abstract domain for data, like octagons, for comparing data elements).
We propose a radically new approach to heap analysis through an abstract
domain of automata, called automatic shapes (automatic because we use automata). The abstract domain uses a particular kind of automata, called quantified data automata, that define, logically, universally quantified properties of
heap structures. In this paper, we restrict our attention to heap structures that
have only one pointer field ; our analysis is hence one that can be used to analyze
properties of heaps containing lists, with possible aliasing (merging) of them, especially at intermediate stages in the program. One-pointer heaps can be viewed
as skinny trees (trees where the number of branching nodes is bounded).
Automata, in general, are classical ways to capture an infinite set of objects
using finite means. A class of (regular) skinny trees can hence be represented
using tree automata, capturing the structure of the heap. While similar ideas
have been explored before in the literature [17], our main aim is to also represent
properties of the data stored in the heap, building automata that can express
universally quantified properties on lists, in particular those of the form
V

i

∀x. (Guardi (p, x) ⇒ Datai (d(p), d(x)))

where p is the set of static pointer variables in the program. The Guardi formulas express structural constraints on the quantified variables and the pointer
variables, while the Datai formulas express properties about the data stored at
the nodes pointed to by these pointers. In this paper, we investigate an abstract
domain that can infer such quantified properties, parameterized by an abstract
numerical domain Fd for the data formulas and by the number of quantified
variables x.
The salient aspect of the automatic shapes that we build is that (a) there
is no requirement from the user to define instrumentation predicates for the
structural Guard formulas; (b) since the abstraction will not be done by merging
unary predicates and since the automata can define how data stored at multiple
locations on the heap are related, there is no need for the user to define carefully
crafted unary predicates that relate structure and data (e.g., like the unary
predicate s(x) defined above that says that the location x is sorted with respect
to all successive locations that come after x but before i). Despite this lack of
help from the user, we show how our abstract domain can infer properties of
a large number of list-manipulating programs adequately to prove interesting
quantified properties.
The crux of our approach is to use a class of automata, called quantified
data automata on skinny trees (QSDA), to express a class of single-pointer
2

heap structures and the data contained in them. QSDAs read skinny trees with
data along with all possible valuations of the quantified variables, and for each
of them check whether the data stored in these locations (and the locations
pointed to by pointer variables in the program) relate in particular ways defined
by the abstract data-domain Fd . We show that the class of QSDAs (over a
data-domain Fd and a set of variable x) forms an abstract data domain lattice.
Along with the natural concretization and abstraction relations, this class forms
a Galois connection with respect to the class of concrete single-pointer heap data
structures.
We further show, for a simple heap-manipulating programming language,
that we can define an abstract post operator over the abstract domain of QSDAs.
This abstract post preserves the structural aspects of the heap precisely (as
QSDAs can have an arbitrary number of states to capture the evolution of
the program) and that it soundly abstracts the quantified data properties. The
abstract post is nontrivial to define and show it effective as it requires automatatheoretic operations that need to simultaneously preserve structure as well as
data properties; this forms the hardest technical aspect of our paper. We thus
obtain an effective abstract interpretation using the domain of QSDAs.
Traditionally, in order to handle loops and reach termination, abstract domains require some form of widening. Our notion of widening is directed by
decidability considerations. Assume that the programmer computes a QSDA as
an invariant for the program at a particular point, where there is an assertion
expressed as a quantified property p over lists (such as “the list pointed to by
head is sorted”). In order to verify that the abstraction proves the assertion, we
will have to check if the language of lists accepted by the QSDA is contained
in the language of lists that satisfy the property p. However, this is in general
undecidable. Our aim is to overapproximate the QSDA into a larger language
accepted by a particular kind of data automata, called elastic QSDA (EQSDA)
for which this inclusion problem is decidable (for an appropriately chosen language for expressing assertions).
This elastification will in fact serve as the basis for widening as well, as there
are only a finite number of elastic QSDAs that express structural properties,
discounting the data-formulas. Consequently, we can combine the elastification
procedure (which overapproximates a QSDA into an elastic QSDA) and widening over the numerical domain for the data in order to obtain widening procedures that can be used to accelerate the computation for loops. In fact, the
domain of EQSDAs can be seen as an abstract domain, and there is a natural abstract interpretation between QSDAs and EQSDAs, where the EQSDAs
permit widening procedures. We show a unique elastification theorem that shows
that for any QSDA, there is a unique elastic QSDA that over-approximates it.
This elastification is in fact the abstract map α that connects QSDAs with
EQSDAs (the γ map being identity, as EQSDAs are also QSDAs).
We also show that EQSDA properties over lists can be translated to a decidable fragment of the logic Strand [21] over lists, and hence inclusion checking
an elastic QSDA with respect to any assertion that is also written using the
3

decidable sublogic of Strand over lists is decidable. The notion of QSDAs and
elasticity are extensions of recent work in [12], where such notions were developed for words (as opposed to trees) and where the automata were used for
learning invariants from examples and counter-examples.
We implement our abstract domain and transformers and show, using a
suite of list-manipulating programs, that our abstract interpretation is able
to prove the naturally required (universally-quantified) properties of these programs. While several earlier approaches (such as shape analysis) can tackle the
correctness of these programs as well, our abstract analysis is able to do this
without requiring program-specific help from the user (for example, in terms of
instrumentation predicates in shape analysis, and in terms of guard patterns in
the work by Bouajjani et al [6]).
Related Work. Shape analysis [29] is the one of the most well-known technique for synthesizing invariants about dynamically evolving heaps. However,
shape analysis requires user-provided instrumentation predicates which are often too particular to the program being verified. Hence coming up with these
instrumentation predicates is not an easy task. In recent work [6, 7, 15, 24], several abstract domains have been explored which combine the shape and the data
constraints. Though some of these domains [7, 24] can handle heap structures
more complex than singly-linked lists, all these domains require the user to provide a set of data predicates [15] or a set of structural guard patterns [6] or
predicates over both the structure and the data constraints [7, 24]. In contrast,
the only assistance our technique requires from the user is specifying the number
of universally quantified variables.
For singly-linked lists, [23] introduces a family of abstractions based on a set
of instrumentation predicates which track uninterrupted list segments. However
these abstractions only handle structural properties and not the more-complex
quantified data properties. Several separation logic based shape analysis techniques have also been developed over the years [4, 5, 11, 16]. But they too mostly
handle only the shape properties (structure) of the heap.
Our automaton model for representing quantified invariants over lists is inspired by the decidable fragment of Strand [21] and can track invariants with
guard constraints of the form y ≤ t or t ≤ y for a universal variable y and some
term t. These structural constraints on the guard are very similar to array partitions in [9,14,18]. However, our automata model is more general. For instance,
none of these related works can handle sortedness of arrays which requires quantification over more than one variable.
Techniques based on Craig’s interpolation have recently emerged as an orthrogonal way for synthesizing quantified invariants over arrays and lists [1,
20, 25, 30]. These methods use different heuristics like term abstraction [30] or
introduction of existential ghost variables [1] or finding interpolants over a restricted language [20, 25] to ensure the convergence of the interpolant from a
small number of spurious counter-examples. The shape analysis proposed in [28]
is also counter-example driven. [28] requires certain quantified predicates to be
provided by the user. Given these predicates, it uses a CEGAR-loop for incre4

mentally improving the precision of the abstract transformer and also discovering
new predicates on the heap objects that are part of the invariant.
Automata based abstract interpretation has been explored in the past [17]
for inferring shape properties about the heap. However, in this paper we are
interested in strictly-richer universally quantified properties on the data stored in
the heap. [2] introduces a streaming transducer model for algorithmic verification
of single-pass list-processing programs. However the transducer model severely
constrains the class of programs it can handle; for example, [2] disallows repeated
or nested list traversals which are required in sorting routines, etc.
In this paper we introduce a class of automata called quantified skinnytree data automata (QSDA) to capture universally quantified properties over
skinny-trees. The QSDA model is an extension of recent work in [12] where a
similar automata model was introduced for words (as opposed to trees). Also,
the automata model in [12] was parameterized by a finite set of data formulas
and was used for learning invariants from examples and counter-examples. In
contrast, we extend the automata in [12] to be instantiated with a (possiblyinfinite) abstract domain over data formulas and develop a theory of abstract
interpretation over QSDAs.

2

Programs Manipulating Heap and Data

We consider sequential programs manipulating acyclic singly-linked data structures. A heap structure is composed of locations (also called nodes). Each location is endowed with a pointer field next that points to another location or it
is undefined, and a data field called data that takes values from a potentially
infinite domain D (i.e. the set of integers). For simplicity we assume a special
location, called dirty, that models an un-allocated memory space. We assume
that the next pointer field of dirty is undefined. Besides the heap structure, a
program also has a finite number of pointer variables each pointing to a location
in the heap structure, and a finite number of data variables over D. In our programming language we do not have procedure calls, and we handle non-recursive
procedures calls by inlining the code at call points. In the rest of the section we
formally define the syntax and semantics of these programs.
Syntax. The syntax of pro- hprgmi ::= pointer p1 , . . . , pk ; data d1 , . . . , dℓ ; hpc stmti+
grams is defined by the BNF hpc stmti ::= pc : hstmti;
hstmti ::= hctrl stmti | hheap stmti
grammar of Figure 1. A pro- hctrl stmti ::= d :=hdata expr i | skip | assume(hpredi)
i
gram starts with the dec| if hpredi then hpc stmti+ else hpc stmti+ fi
| while hpredi do hpc stmti+ od
laration of pointer variables
among which one called hheap stmti ::= new pi | pi := nil | pi := pj
| pi := pj → next | pi → next := nil | pi → next := pj
nil, followed by a declara| pi → data := hdata expr i
tion of data variables. Data
Fig. 1: Simple programming language.
variables range over a potentially infinite data domain D. We assume a language of data expressions
built from data variables and terms of the form pi → data (with pi 6= nil)
5

using operations over D. Predicates in our language are either data predicates
built from predicates over D or structural predicates concerning the heap built
from atoms of the form pi == pj , pi → next == pj , and pi →∗ next == pj ,
for some i, j ∈ [1, k]. Thereafter, there is a non-empty list of labelled statements
of the form pc : hstmti where pc is the program counter and hstmti defines a
language of either C-like statements or statements which modify the heap. We
do not have an explicit statement to free locations of the heap: when a location
is no longer reachable from any location pointed by a pointer variable we assume
that it automatically disappears from the memory. For a program P , we denote
with PC the set of all program counters of P statements. Figure 2(a) shows the
code for program sorted list-insert which is a running example in the paper. The
program inserts a key into the sorted list pointed to by variable head.
Semantics. A configuration C of a program P with set of pointer variables PV
and data variables DV is a tuple hpc, H, pval , dval i where
– pc ∈ PC is the program counter of the next statement to be executed;
– H is a heap configuration represented by a tuple (Loc, next, data) where
(1) Loc is a finite set of heap locations containing a special element called
dirty, (2) next : Loc 7→ Loc is a partial map defining an edge relation among
locations such that the graph (Loc, next) is acyclic, and (3) data : Loc 7→ D
is a map that associates each location of Loc with a data value in D;
– pval : PV 7→ Loc associates each pointer variable of P with a location in H.
If pval (p) = v we say that node v is pointed by variable p. Furthermore, each
node in Loc is reachable from a node pointed by a variable in PV . There is
no outgoing (next) edge from location dirty and there is a next edge from
the location pointed by nil to dirty;
– dval : DV 7→ D is a valuation map for the data variables.
Figure 2(b) graphically shows a progam configuration which is reachable at
program counter 8 of the program in Figure 2(a) (as explained later we encode
the data variable key as a pointer variable in the heap configuration). The transtmt
sition relation of a program P , denoted −−−→P for each statement stmt of P ,
is defined as usual. The control-flow statements update the program counter,
possibly depending on a predicate (condition). The assignment statements update the variable valuation or the heap structure other than moving to the next
program counter. A formal semantics of programs can be found in Appendix A.
stmt
Let us define the concrete transformer F ♮ = λC.{C ′ | C −−−→P C ′ }. The concrete
semantics of a program is given as the least fixed point of a set of equations of
the form ψ = F ♮ (ψ).
To simplify the presentation of the paper, we assume that our programs do
not have data variables. This restriction, indeed, does not reduce their expressiveness: we can always transform a program P into an equivalent program P ′
by translating each data variable d into a pointer variable that will now point
to a fresh node in the heap structure, in which the value d is now encoded by
d → data. The node pointed by d is not pointed by any other pointer, further,
6

d → next points to dirty. Obviously, wherever d is used in P will now be replaced
by d → data in P ′ .

3

Quantified Skinny-Tree Data Automata

In this section we define quantified skinny-tree data automata (QSDAs, for
short), an accepting mechanism of program configurations (represented as special
V labelled trees) on which we can express properties of the form
i ∀y1 , . . . , yℓ . Guardi ⇒ Datai , where variables yi range over the set of locations
of the heap, Guardi represent quantifier-free structural constraints among the
pointer variables and the universally quantified variables yi , and Datai (called
data formulas) are quantifier-free formulas that refer to the data stored at the
locations pointed either by the universal variables yi or the pointer variables,
and compare them using operators over the data domain. In the rest of this
section, we first define heap skinny-trees which are a suitable labelled tree encodings for program configurations; we then define valuation trees which are heap
skinny-trees by adding to the labels an instantiation of the universal variables.
Quantified skinny-tree data automata is a mechanism designed to recognize valuation trees. The language of a QSDA is the set of all heap skinny-trees such that
all valuation trees deriving from them are accepted by the QSDA. Intuitively,
the heap skinny-trees in the language defined
by the QSDA are all the program
V
configurations that verify the formula i ∀y1 , . . . , yℓ .Guardi ⇒ Datai .
Let T be a tree. A node u of T is branching whenever u has more than
one child. For a given natural number k, T is k-skinny if it contains at most k
branching nodes.
Heap skinny-trees. Let PV be the set of pointer variables of a program P
and Σ = 2PV (let us denote the empty set with a blank symbol b). We associate
with each P configuration C = hpc, H, pval , dval i with H = (Loc, next, data),
the (Σ × D)-labelled graph H = (T, λ) whose nodes are those of Loc, and where
(u, v) is an edge of T iff next(v) = u (essentially we reverse all next edges). From
the definition of program configurations it is easy to see that T is a k-skinny tree
where k = |PV |. The labelling function λ : Loc 7→ (Σ × D) is defined as follows:
for every u ∈ Loc, λ(u) = (S, d) where S is the set of all pointer variables p such
that pval (p) = u, and d = data(u). We call H the heap skinny-tree of C.
In general heap skinny-trees can be logically characterized as follows.
Definition 1 (Heap Skinny-Trees). A heap skinny-tree over a set of pointer
variables PV (with nil∈ PV ) and data domain D, is a (Σ ×D)-labelled k-skinny
tree (T, λ) with Σ = 2PV and k = |PV |, such that:
– for every leaf v of T , λ(v) = (S, d) where S 6= ∅;
– for every pointer variable p ∈ PV , there is a unique node v of T such that
λ(v) = (S, d) with p ∈ S;
– the node v of T such that λ(v) = (S, d) and nil∈ S is one of the childen of
the root of T .
⊓
⊔
7

prev

head

pointer head, cur , prev, tmp;
data key;

2

1: cur := head;
2: while (cur! = nil∧
cur → data < key) do
3:
prev := cur ;
4:
cur := cur → next;
od
5: new tmp;
({nil}, $)
6: tmp → data := key;
7: tmp → next := cur ;
8: if (prev ! = nil) then
({cur}, 9)
9:
prev → next := tmp;
else
({prev}, 6)
10:
head := tmp;
fi

(b)

(a)

(c)

cur
6

tmp

nil
9

8

key

8

(b, −, $)

(b, $)
({key}, 8)

$

$

({nil}, −, $)

({key}, −, 8)

({cur }, y2 , 9)
({tmp}, 8)

({head}, 2)

({prev}, y1 , 6)

(d)

({tmp}, −, 8)

({head}, −, 2)

Fig. 2: (a) sorted list-insert program P ; (b) shows a P configuration at program
counter 8; (c) is the heap skinny-tree associated to (b); (d) is a valuation tree
of (c).

Figure 2(c) shows the heap skinny-tree corresponding to the program configuration of Figure 2(b). Note that though the program handles a singly linked
list, in the intermediate operations we can get trees. However they are special
trees with bounded branching. This example illustrates that program configurations of list manipulating programs naturally correspond to heap skinny-trees.
It also motivates why we need to extend automata over words introduced in [12]
to quantified data automata over skinny-trees. We now define valuation trees.
Valuation trees. Let us fix a finite set of universal variables Y . A valuation tree
over Y of a heap skinny-tree H is a (Σ × (Y ∪ {−}) × D)-labelled tree obtained
from H by adding an element from the set Y ∪ {−} to the label, in which every
element in Y occurs exactly once in the tree. We use the symbol ‘−’ at a node v
if there is no variable from Y labelling v. A valuation tree corresponding to the
heap skinny-tree of Figure 2(c) is shown in Figure 2(d).
Definition 2 (Quantified Skinny-Tree Data Automata). A quantified
skinny-tree data automaton (QSDA) over a set of pointer variables PV (with
|PV | = k), a data domain D, a set of universal variables Y , and a set of data
formulas F over D, is a tuple A = (Q, Π, ∆, T , f ) where:
– Q is a finite set of states;
– Π = Σ × Yb is the alphabet where Σ = 2P V and Yb = Y ∪ {−};
– ∆ = (∆0 , ∆1 , . . . , ∆k ) where, for every i ∈ [1, k], ∆i : (Qi × Π) 7→ Q defines
a (deterministic) transition relation;
– T : Q → 2P V ∪Y is the type associated with every state q ∈ Q;
– f : Q 7→ F is a final-evaluation.
⊓
⊔
8

A valuation tree (T, λ) over Y of a program P , where N is the set of nodes
of T , is recognized by a QSDA A if there exists a node-labelling map ρ : N 7→ Q
that associates each node of T with a state in Q such that for each node t of
T with λ(t) = (S, y, d) the following holds (here λ′ (t) = (S, y) is obtained by
projecting out the data values from λ(t)):
is a leaf then ∆0 (λ′ (t)) = ρ(t) and (T (ρ(t)) ∩ PV ) 6= ∅.
is an internal node, with sequence of children t1 , t2 , . . . , ti then
∆i ( (ρ(t1 ), . . . , ρ(ti )), λ′ (t) ) = ρ(t);
S ∩ T (ρ(tj )) = ∅ and 
y∈
/ T (ρ(tj )), for 
every j ∈ [1, i];
S
T (ρ(t)) = S ∪ {y} ∪
T (ρ(tj )) if y ∈ Y . Otherwise if y = −
S j∈[1,i]

then T (ρ(t)) = S ∪
T
(ρ(t
))
.
j
j∈[1,i]
– if t is the root then T (ρ(t)) = (PV ∪ Y ) and the formula f (ρ(t)), obtained
by replacing all occurrences of terms y → data and p → data with their
corresponding data values in the valuation tree, holds true.
– if t
– if t
•
•
•

A QSDA can be thought as a register automaton that reads a valuation
tree in a bottom-up fashion and stores the data at the positions evaluated for
Y and locations pointed by elements in PV , and checks whether the formula
associated to the state at the root holds true by instantiating the data values
in the formula with those stored in the registers. Furthermore, the role of map
T is that of enforcing that each element in PV ∪ Y occurs exactly once in the
valuation tree.
A QSDA A accepts a heap skinny-tree H if A recognizes all valuation trees
of H. The language accepted by A, denoted L(A), is the set of all heap skinnytrees H accepted by A. A language L of heap skinny-trees is regular if there is
a QSDA A such that L = L(A). Similarly, a language L of valuation trees is
regular if there is a QSDA A such that L = Lv (A), where Lv (A) is the set of
all valuation trees recognized by A.
QSDAs are a generalization of quantified data automata introduced in [12]
that handle only lists as opposed to QSDAs that handle skinny-trees. We now
introduce various characterizations of QSDAs which are used later in the paper.
Unique minimal QSDA. In [12] the authors show that it is not possible to
have a unique minimal quantified data automaton over words (with respect to the
number of states) which accepts a given language over linear heap configurations.
The proof gives a set of heap configurations over a linear heap-structure which is
accepted by two different automata having the same number of states. Since QSDAs are a generalization of quantified data automata, the same counter-example
language holds for QSDAs. However, under the assumption that all data formulas in F are pairwise non-equivalent, there does exist a canonical automaton
on the level of valuation trees. In [12], the authors prove the canonicity of quantified data automata, and their result extends to QSDAs in a straight forward
manner.
Theorem 1. For each QSDA A there is a unique minimal QSDA A′ such that
Lv (A) = Lv (A′ ).
9

We give some intuition behind the proof of Theorem 1. First, we introduce
a central concept called symbolic trees. A symbolic tree is a (Σ × (Y ∪ {−}))labelled tree that records the positions of the universal variables and the pointer
variables, but does not contain concrete data values (hence the word symbolic).
A valuation tree can be viewed as a symbolic tree augmented with data values at
every node in the tree. There exists a unique tree automaton over the alphabet Π
that accepts a given regular language over symbolic trees. It can be shown that
if the set of formulas in F are pair-wise non-equivalent, then each state q in the
tree automaton, at the root, can be decorated with a unique data formula f (q)
which extends the symbolic trees with data values such that the corresponding
valuation trees are in the given language.
Hence, a language of valuation trees can be viewed as a function that maps
each symbolic tree to a uniquely determined formula, and a QSDA can be
viewed as a Moore machine (an automaton with output function on states) that
computes this function. This helps us separate the structure of valuation trees
(the height of the trees, the cells the pointer variables point to) from the data
contained in the nodes of the trees. We formalize this notion by introducing
formula trees.
Formula trees. A formula tree over pointer variables P V , universal variables
Y and a set of data formulas F is a tuple of a Σ × (Y ∪ {−})-labelled tree
(or in other words a symbolic tree) and a data formula in F such that if we
extend the tree with data values which satisfy the formula, we get a valuation
tree.
V For a QSDA which captures a universally quantified property of the form
i ∀y1 . . . yℓ .Guardi ⇒ Datai , the symbolic tree component of the formula tree
corresponds to guard formulas like Guardi which express structural constraints
on the pointers pointing into the valuation tree. The data formula in the formula
trees correspond to Datai which express the data values with which a symbolic
tree (read Guardi ) can be extended so as to get a valuation tree accepted by the
QSDA. In our running example, consider a QSDA with a formula tree which has
the same symbolic tree as the valuation tree in Figure 2(d) (but without the data
values in the nodes) and a data-formula ϕ = y1 → data ≤ y2 → data ∧ y1 →
data < key ∧ y2 → data ≥ key. This formula tree represents all valuation trees
(including the one shown in Figure 2(d)) which extend the symbolic tree with
data values which satisfy ϕ.
By introducing formula trees we explicitly take the view of a QSDA as
an automaton that reads symbolic trees and outputs data formulas. We say a
formula tree (t, ϕ) is accepted by a QSDA A if A reaches the state q after reading
t and f (q) = ϕ. Given a QSDA A, the language of valuation trees accepted by A
gives an equivalent language of formula trees accepted by A and vice-versa. We
denote the set of formula trees accepted by A as Lf (A). A language over formula
trees is called regular if there exists a QSDA accepting the same language.
Theorem 2. For each QSDA A there is a unique minimal QSDA A′ that
accepts the same set of formula trees.
10

4

QSDAs as an Abstract Domain

In the previous section we introduced quantified skinny-tree data automata as
an automaton model for expressing universally quantified properties over heap
skinny-trees. In this section, we first show that QSDAs form a lattice and then
formalize the correspondence, by establishing an abstraction function and a concretization function, between a set of heap skinny-trees and QSDAs.
Given a set of pointer variables PV and universal variables Y , let QF be
the set of all QSDA over a set of data formulas F . Clearly QF is a partiallyordered set where the most natural partial order is the set-inclusion over the
language of QSDAs. However checking whether a pair of QSDAs are ordered
with respect to this partial order is undecidable. Since QSDAs generalize the
quantified data automata over words [12], the undecidability follows from the
fact that quantified data automata (as well as QSDAs) can express quantified
invariants such that checking the validity of such invariants is undecidable.
So, we consider a new partial-order on QSDAs which is decidable, allows us to
define a unique least upper bound for every pair of QSDAs and finally show that
QSDAs form a lattice. To accomplish this, let us first assume that the set of formulas F parameterizing QSDAs form a lattice F = (F, ⊑F , ⊔F , ⊓F , false, true)
where ⊑F is the partial-order on the data-formulas, ⊔F and ⊓F are the least
upper bound and the greatest lower bound and false and true are formulas required to be in F and correspond to the bottom and the top elements of the
lattice, respectively. Also, we assume that whenever α ⊑F β then α ⇒ β. Furthermore, we assume that any pair of formulas in F are non-equivalent. For a
logical domain as ours, this can be achieved by having a canonical representative
for every set of equivalent formulas.
Now if we view a QSDA as a mapping from symbolic trees to formulas in
F , we can define a new partial-order relation on QSDAs as follows. We say
A1 ⊑ A2 if Lf (A1 ) ⊆ Lf (A2 ), which means that for every symbolic tree t if
(t, ϕ1 ) ∈ Lf (A1 ) and (t, ϕ2 ) ∈ Lf (A2 ) then ϕ1 ⊑F ϕ2 . Note that, whenever
A1 ⊑ A2 implies that L(A1 ) ⊆ L(A2 ). Also, with respect to this new partial
order, we can show that QSDAs form a complete lattice (QF , ⊑, ⊔, ⊓, ⊥, ⊤)
where the join of the two automata A1 and A2 maps the symbolic tree t to the
unique formula ϕ1 ⊔F ϕ2 . Similarly, the meet of the automata A1 and A2 maps
the tree t to ϕ1 ⊓F ϕ2 . The bottom element in the lattice QF is the QSDA which
maps every symbolic tree to false and the top element is the QSDA which maps
every symbolic tree to the formula true.
We now define an abstraction function α : H → QF and a concretization
function γ : QF → H such that (H, α, γ, QF ) form a Galois-connection. Note
that, abstract interpretation [8] requires that the abstraction function α maps
a concrete element (a language of heap skinny-trees) to a unique element in the
abstract domain and that α be surjective; similarly γ should be an injective
function. Also note that given a regular language of heap skinny-trees there
might be several QSDAs accepting that language. In such a case defining a
surjective function α is not possible. Therefore, we first restrict ourselves to a
set of QSDAs in QF where each QSDA accepts a different language. Under this
11

assumption,dwe define an α and a γ as follows: for a set of heap configurations
H, α(H) = {A | H ⊆ L(A)} and γ(A) = {H | H ∈ L(A)}. Note that both α
and γ are order-preserving; α is surjective and γ is an injective function. Also for
a set of heap configurations H, H ⊆ γ(α(H)) and for a QSDA A, A = α(γ(A)).
Hence (H, α, γ, QF ) form a Galois-connection.
Theorem 3. Let (H, ⊆) be the set of all heap skinny-trees and (QF , ⊑) be the
set of QSDAs (accepting pairwise inequivalent languages) over data formulas F ,
then (H, α, γ, QF ) form a Galois-connection.

5

Abstract Semantics over QSDAs

In the previous section we established a Galois-connection between a set of
heap skinny-trees and QSDAs. Here, we describe an abstract transformer over
QSDAs which soundly over-approximates the concrete semantics of the programming language. This provides a way to compute the semantics of a program
over an abstract domain consisting of QSDAs.
We first show that it is not possible to capture the most-precise concrete
transformer on QSDAs. A QSDA expresses universally quantified properties
over heap trees, of the form ∀y1 . . . yℓ .ψ where ψ is a quantifier-free formula
over the pointer variables PV , the universal variables Y and the data value
at the locations pointed to by these variables. Given a QSDA A, the concrete
transformer F ♮ guesses a pre-state accepted by A (which involves existential
quantification), and then constrains the post-state with respect to this guessed
pre-state according to the semantics of the statement. For instance, consider the
statement pi := pj . Given a QSDA accepting a universally quantified property
∀y1 . . . yℓ .ψ, its strongest post-condition with respect to this statement is the
formula: ∃p′i .∀y1 . . . yℓ .ψ[pi /p′i ] ∧ pi = pj . Note that, an interpretation of the
existentially quantified variable p′i in a model of this formula gives the location
node pointed to by variable pi in the pre-state, such that the formula ∀y1 . . . yℓ .ψ
was satisfied by the pre-state. However it is not possible to express these precise
post-conditions, which are usually of the form ∃∗ ∀∗ ψ, in our automaton model.
So we abstract these precise post-conditions by a QSDA which semantically
moves the existential quantifiers inside the universally quantified prefix, where
they can be eliminated. In the above example, the abstract post-condition QSDA
guesses a position for the pointer variable pi for every valuation of the universal
variables, such that the valuation tree augmented with this guessed position is
accepted by the precondition QSDA. More generally, the abstract transformer
computes the most precise post-condition over the language of valuation trees
accepted by a QSDA, instead of computing the precise post-condition over the
language of heap skinny-trees. In fact, we go beyond valuation trees to formula
trees; the abstract transformer evolves the language of formula trees accepted
by a QSDA by tracking the precise set of symbolic trees to be accepted in the
post-QSDA and their corresponding data formulas.
12

Abstract Transformer Ff♯ on a regular language over formula trees

F
pi := nil
λLf . (t′ , ϕ′ ) | ϕ′ : {∃d.ϕ[pi → data/d] | (t, ϕ) ∈ Lf , update(t, pi := nil, t′ )}
′
′
′
pi := pj
λLf . (t , ϕ ) | ϕ : F
(pi → data = pj → data) ⊓
{∃d.ϕ[pi → data/d] | (t, ϕ) ∈ Lf , update(t, pi := pj , t′ )}
 ′ ′
F
pi := pj → next λLf . (t , ϕ ) | ϕ′ : {∃d.ϕ[pi → data/d] | (t, ϕ) ∈ Lf , update(t, pi := pj → next, t′ )}
⊓ (p → data = v → data), v ∈ label(t′ , pi )

F i
pi → next := nil λLf . (t′ , ϕ′ ) | ϕ′ : {ϕ | (t, ϕ) ∈ Lf , update(t, pi → next := nil, t′ )}
F
pi → next := pj λLf . (t′ , ϕ′ ) | ϕ′ : {ϕ | (t, ϕ) ∈ Lf , update(t, pi → next := pj , t′ )}
′
′
′
pi → data :=
λLf . (t , ϕ ) | ϕ : ∃d.ϕ[v
d 1 → data/d, . . . , vℓ → data/d]
data expr
⊓ {v → data = data expr | v ∈ V },
V = {v1 , . . . , vℓ } = label(t′ , pi ), (t′ , ϕ) ∈ Lf

assume ψstruct
λLf . (t′ , ϕ′ ) | (t′ , ϕ′ ) ∈ Lf , t′ |= ψstruct
assume ψdata
λLf . (t′ , ϕ′ ) | ϕ′ : ϕ ⊓ ψdata , (t′ , ϕ) ∈ Lf
′
new pi
λLf . (tF
, ϕ′ ) | ϕ′ : (y → data = pi → data)⊓
{∃d1 d2 .ϕ[pi → data/d1 , y → data/d2 ] | (t, ϕ) ∈ Lf , update(t, newy pi , t′ )},
y ∈ Y ∪ {−}
Statements

Table 1: Abstract Transformer Ff♯ . The abstract transformer F ♯ = λA.A′ where A′ is
the unique minimal QSDA such that Lf (A′ ) = (Ff♯ ) Lf (A). The predicate update and
the set label are defined below.

Table 13 gives the abstract transformer Ff♯ which takes a regular language
over formula trees Lf and gives, as output, a set of formula trees. We know
from Theorem 2 that for any regular set of formula trees there exists a unique
minimal QSDA that accepts it. We show below (see Lemma 1) that for a QSDA
A, the language over formula trees given by (Ff♯ ) Lf (A) is regular. Hence, we
can define the abstract transformer F ♯ as F ♯ = λA.A′ where A′ is the unique
minimal QSDA such that Lf (A′ ) = (Ff♯ ) Lf (A).
In Table 1, label(t, pi) is the set of pointer and universal variables which label
the same node in t as variable pi . The predicate update(t, stmt, t′ ) is true if symbolic trees t and t′ are related such that the execution of statement stmt updates
precisely the symbolic tree t to t′ . As an example, the abstract transformer for
the statement pi := nil in the first row of Table 1 states that the post-QSDA
maps the symbolic tree t′ to the data-formula ϕ′ where ϕ′ is the join of all formulas of the form ∃d.ϕ[pi → data/d] where ϕ is the data-formula associated
with symbolic tree t in the pre-QSDA such that update(t, pi := nil, t′ ) is true.
We now briefly describe the predicate update(t, newy pi , t′ ) which is used
in the definition of the transformer for the new statement and is slightly more
involved. The statement new pi allocates a new memory location. After the execution of this statement, pointer pi points to this allocated node. Besides, the
universal variables also need to valuate over this new node apart from the valuations over the previously exisiting locations in the heap. The superscript y in
the predicate update(t, newy pi , t′ ) tracks the case when variable y ∈ Y ∪ {−}
valuates over the newly allocated node. Hence, if update(t, newy pi , t′ ) holds true
then the symbolic trees t and t′ agree on the locations pointed to by all variables
3

The abstract transformer defined in Table 1 assumes that there are no memory errors
in the program. It can be extended to handle memory errors.

13

except pi and the universal variable y; both these variables point, in t′ , to a new
location v which is not in t and a new edge exists in t′ from the root to v.
From the construction in Table 1 it can be observed that given a language of
valuation trees obtained uniquely from a language of formula trees, Ff♯ applies
the most-precise concrete transformer on each valuation tree in the language,
and then constructs the smallest regular language of valuation trees (or equivalently formula trees) which approximates this set. More precisely, for all formula
trees (t, ϕ) ∈ Lf (A), the abstract transformer Ff♯ applies the precise concrete
transformer on the symbolic tree t (only the structure with the valuations for
universal variables) to obtain t′ . And separately, it applies the precise concrete
transformer on the data extensions of t, which is given by ϕ, to obtain the data
formula ϕ′ such that (t′ , ϕ′ ) ∈ (Ff♯ )Lf (A). However, note that reasoning over
valuation/formula trees (and not heap skinny-trees) comes with a loss in precision. To regain some of this lost precision, we define a function Strengthen which
takes a formula language Lf and finds a smaller language over formula trees,
which accepts the same set of heap trees. Here t ⇂y stands for a Π\{y} -labelled
tree which agrees with t on the locations pointed to by all variables except y.

Strengthen = λy.λLf . (t′ ,ϕ′ ) | ϕ′ : ϕ′′ ⊓ φ, (t′ , ϕ′′ ) ∈ Lf ,
l
φ : {∃d.ϕ[y → data/d] | (t, ϕ) ∈ Lf , t ⇂y = t′ ⇂y }
We now reason about the soundness of the operator Strengthen. Fix a y ∈ Y .
Consider a QSDA A with a language over formula trees Lf and consider all symbolic trees t such that t ⇂y = t′ ⇂y . This implies that the trees t have the pointer
variables pointing to the same positions as t′ and have the same valuations for
variables in Y \{y}. Since our automaton model has a universal semantics, any
heap tree accepted by A should satisfy the data formulas annotated at the final
states reached for every valuation of the universal variables. If we look at a fixed
valuation for variables in Y \{y} (which is same as that in t′ ) and different valuations for y, any heap tree accepted should satisfy the formula ∃d.ϕ[y → data/d]
for all such (t, ϕ) ∈ Lf . Hence the Strengthen operator can safely strengthen the
formula ϕ′′ associated with the symbolic tree t′ to ϕ′′ ⊓ φ. Appendix C shows
that for a given universal variable y and a regular language Lf , the language
over formula trees (Strengthen) y Lf is regular. The proof in fact constructs
the QSDA accepting the language (Strengthen) y Lf (A) for a QSDA A. The
abstract transformer Ff♯ can be thus soundly strengthened by an application of
Strengthen at each step, for each variable y ∈ Y .
We now prove that the language over formula trees given by (Ff♯ )Lf (A) is
a regular language for any QSDA A. This helps us to construct the abstract
transformer F ♯ : QF → QF . And finally, we show that this abstract transformer
is a sound approximation of the concrete transformer F ♮ .
Lemma 1. For a QSDA A, the language (Ff♯ ) Lf (A) over formula trees is
regular.
Proof. We prove via construction. Given a QSDA A, we construct a QSDA A′
such that Lf (A′ ) = (Ff♯ ) Lf (A).
14

Here we only give the construction of A′ for the statement pi := nil (for other
statements, see Appendix D). The QSDA A′ simulates A on all the nodes, except
a node v labeled with pointer pi and the node labeled nil. A tree accepted by
A′ does not read pi at node v; on the other hand pi is read at the nil node.
Let A = (Q, Π, ∆, T , f ), then A′ is of the form (Q, Π, ∆′ , T ′ , f ′ ). For every
transition ∆(q1 , . . . , qj , π) = q such that pi and nil are not present in the label
π, ∆′ (q1 , . . . , qj , π) = q. However if pi is present in π and nil is not, then the
corresponding transition in A′ is ∆′ (q1 , . . . , qj , π ′ ) = q where π ′ is same as π
except it does not have pi . On the other hand, if nil is present in π and pi is
not, then the transition ∆′ (q1 , . . . , qj , π ′ ) = q where π ′ is same as π except for
the presence of pi . The new type T ′ can be easily computed for every state in
the automaton. The evaluation function f ′ existentially quantifies out the data
value of pointer pi i.e. for all states q ∈ Q, f ′ (q) = ∃d.f (q)[pi → data/d]. The
transition relation ∆′ thus constructed might need to be determinized to obtain
A′ . For a symbolic tree t and formulas ϕ1 , . . . , ϕj such that (t, ϕ1 ), . . . , (t, ϕj )
belong to the language, the determinization procedure maps t to the formula
ϕ1 ⊔ . . . ⊔ ϕj . It can be easily shown that the language of A′ is (F ♯ ) Lf (A).
Appendix D shows the construction of the automaton A′ for other statements in our language. In this way, via construction, we prove that the language
(F ♯ ) Lf (A) over formula trees is regular.
⊓
⊔
From Lemma 1 and Theorem 2 it follows that there exists a QSDA A′ such
that A′ = (F ♯ )A. In fact the proof of Lemma 1 constructs such an automaton
A′ . The monotonicity of F ♯ with respect to F ♮ follows from the monotonicity of
Ff♯ . The soundness of F ♯ can be stated as the following theorem.
Theorem 4. The abstract transformer F ♯ is sound with respect to the concrete
transformer F ♮ .
Proof. We prove the soundness of F ♯ by showing that F ♮ ◦ γ ⊑ γ ◦ F ♯ . Let us
consider a QSDA A and a heap skinny-tree H such that H ∈ L(A). Consider
a statement stmt such that H gets transformed to H′ on the execution of stmt
♮
i.e. Fstmt
(H) = H′ . We would like to prove that H′ ∈ L(F ♯ (A)).
To prove this, consider a valuation of universal variables Y over the nodes in
H′ . Let the corresponding symbolic tree be t′ and let the data values in H′ at
the positions pointed to by Y be given by r′ : Y → D. Let us assume that the
QSDA F ♯ (A) maps the symbolic tree t′ to the formula ϕ′ . Then, we would like
to prove that r′ |= ϕ′ . By arguing over all valuations over H′ , this would prove
that H′ ∈ L(F ♯ (A)).
To prove that r′ |= ϕ′ , fix a valuation of the universal variables Y over the
nodes in H such that the corresponding symbolic tree t satisifes update(t, stmt, t′ )
(for statements which do not modify the structure of the heap, t = t′ ). Let the
data values at the positions pointed to by universal variables Y in H be given by
r. Since H ∈ L(A), if A maps the symbolic tree t to the formula ϕ then r |= ϕ.
The abstract transformer Ff♯ applies the precise concrete transformer, with respect to only the data values of the heap, to the formula ϕ and over-approximates
15

it to obtain ϕ′ . From the monotonicity of the concrete transformer, this implies
that r′ |= ϕ′ .
⊓
⊔
Since F ♯ is both monotonic and sound, from the Knaster-Tarski theorem,
the set of equations of the form ψ = F ♯ (ψ) expressing the abstract semantics of
a program admit a least fix point solution, and this solution is a sound approximation of the concrete semantics of the program.
Note that the abstract transformer, in general, might require a powerset construction over the input QSDA, very similar to the procedure for determinizing
a tree automaton. Hence the worst-case complexity of the abstract transformer
is exponential in the size of the QSDA. However our experiments show that this
worst-case is not achieved for most programs in practice.
Theorem 5. The abstract semantics of a program, computed with respect to the
abstract transformer F ♯ , is correct.

6

Elastic Quantified Skinny-Tree Data Automata

For a given set of pointer variables PV and universal variables Y , the QSDAs
can be of arbitrarily large size. The number of QSDAs is not bounded and the
computation of the abstract semantics of a program over QSDAs might not
converge. To remedy this problem, we identify a sub-class of QSDAs called elastic quantified skinny-tree data automata (EQSDAs). Elastic QSDAs provide a
mechanism to accelerate the fix-point computation over QSDAs. However, instead of choosing any acceleration mechanism, the elastic QSDAs were chosen
keeping decidability of the invariants they express in mind. A key property in
the decidable fragment of Strand is that it cannot test whether two universally
quantified variables are a bounded distance away. We show in Section 6.1 that
the invariants expressed by EQSDAs fall in the decidable fragment of Strand.
So EQSDAs not only help in guaranteeing the convergence of the abstract semantics of a program, but also ensure that a program, if annotated with a set of
assertions over logical formulas in Strand, can be proved correct by validating
those assertions in a decidable manner.
Let us denote the symbol (b, −) ∈ Π indicating that a position does not contain any variable by b. A QSDA A = (Q, Π, ∆, T , f ) where ∆ = (∆0 , ∆1 , . . . , ∆k )
is called elastic if each transition on b in ∆1 is a self loop i.e. ∆1 (q1 , b) = q2 implies q1 = q2 .
We first show that the number of EQSDAs is bounded for a fixed set PV and
Y . Recall that heap skinny-trees accepted by QSDAs require that the number
of branching nodes in the skinny trees are bounded. So, the only infinity in the
size of a skinny-tree is due to an unbounded number of b-labelled nodes which
might occur along linear segments of the tree. If we simulate an elastic QSDA on
a skinny-tree accepted by it, all consecutively occurring b-labelled nodes along
linear segments of the tree are labelled with the same state (due to the elasticity
property). To count the maximum number of states, in an EQSDA, required
to accept a language over heap trees, we might as well consider only those trees
16

in the language which have no b-labelled nodes occurring along linear segments
in the tree. For a given set PV and Y , the number of such skinny-trees and
their sizes are bounded. This bounds the number of states in an EQSDA which
accepts any language over heap skinny-trees. This also proves that for a given
PV and Y , the number of EQSDAs are bounded.
We next show the following result that every QSDA A can be uniquely overapproximated by a language of valuation trees (or equivalently formula trees)
that can be accepted by an EQSDA Ael . We will refer to this construction, which
we outline below, as elastification. This result is an extension of the unique overapproximation result for quantified data automata over words [12]. Using this
result, we can show that elastic QSDAs form a finite join semi-lattice and there
exists a Galois-connection hαel , γ el i between QSDAs and the set of EQSDAs.
This lets us define an abstract transfomer over the abstract domain EQSDAs
such that the semantics of a program can be computed over EQSDAs (it terminates) in a sound manner.
Let A = (Q, Π, ∆, T , f ) be a QSDA such that ∆ = (∆0 , ∆1 , . . . , ∆k ) and
for a state q let Rb (q) := {q ′ | q ′ = q or ∃q ′′ .q ′′ ∈ Rb (q) and ∆1 (q ′′ , b) = q ′ } be
the set of states reachable from q by a (possibly
empty) sequence of b-unaryS
transitions. For a set S ⊆ Q we let Rb (S) := q∈S Rb (q).
The set of states of Ael consists of sets of states of A that are reachable by the
following transition function ∆el (where ∆i (S1 , . . . , Si , a) denotes the standard
extension of the transition function of A to sets of states):
∆el
0 (a) = Rb (∆0 (a))


Rb (∆1 (S, a))
∆el
S
1 (S, a) =


undefined

if a 6= b
if a = b and ∆1 (q, b) is defined for some q ∈ S
otherwise.

∆el
i (S1 , . . . , Si , a) = Rb (∆i (S1 , . . . , Si , a)) for i ∈ [2, k]

Note that this construction is similar to the usual powerset construction except
that in each step we apply the transition function of A to the current set of states
and take the b-closure. However, if the input letter is b on a unary transition,
Ael loops on the current set if a b-transition is defined for some state in the set.
It can be argued inductively, starting from the leaf states, that the type for
all states in a set is the same. Hence we define the type of a set S as the type of
any state in S. The final evaluation formula for aFset is the least upper bound
of the formulas for the states in the set: f el (S) = q∈S f (q). We can now show
that Ael is the most precise over-approximation of the language of valuation
trees accepted by QSDA A.
Theorem 6. For every QSDA A, the EQSDA Ael satisfies Lv (A) ⊆ Lv (Ael ),
and for every EQSDA B such that Lv (A) ⊆ Lv (B), Lv (Ael ) ⊆ Lv (B) holds.
A proof of Theorem 6 is presented in Appendix B and is similar to the proof
of Theorem 3 in [12] for the case of words. The above theorem can also be stated
over a language of formula trees in the same way, that Ael is the most precise
over-approximation of the language of formula trees accepted by QSDA A.
17

Using this result, we next show that EQSDAs form a finite join semi-lattice
(QF el , ⊑, ⊔, ⊥, ⊤). The partial order on EQSDAs is the same as the partial order
on QSDAs but now restricted to elastic QSDAs. For two EQSDAs A1 and A2 ,
the join A1 ⊔ A2 is the unique EQSDA over-approximating A1 ⊔QF A2 . The
bottom and the top elements are the EQSDAs taking every symbolic tree to the
formulas false and true respectively. We can now view the space of EQSDAs as
an abstraction over QSDAs. The abstraction function αel : QF → QF el takes
a QSDA A to its unique over-approximating EQSDA Ael . The concretization
function γ el : QF el → QF is the identity function which maps an EQSDA to
itself. Recall that we had already restricted QF to contain only those QSDAs
which accepted different languages (over heap skinny-trees). Since QF el is a subspace of QF , this restriction extends to it in a natural way. With this assumption
it is easy to see that hαel , γ el i forms a Galois-connection.
Let us define the abstract transformer Fel♯ : QF el → QF el = αel ◦ F ♯ ◦
γel . The soundness of Fel♯ follows from the soundness of F ♯ (and the fact that
hαel , γ el i form a Galois-connection). Similarly its monotonicity follows from the
monotonicity of F ♯ and the monotonicity of αel and γel . The semantics of a
program can be thus computed over the abstract domain QF el as the least fixpoint of a set of equations of the form ψ = Fel♯ (ψ). Since there are a bounded
number of EQSDAs for a given set of program variables PV and universal
variables Y , this least fix-point computation terminates (modulo the convergence
of the data formulas in the formula lattice F in which case termination can be
achieved by defining a suitable widening operator on the data formula lattice).
Theorem 7. The abstract semantics of a program, computed with respect to the
abstract transformer Fel♯ , is computable and is correct.
6.1

From EQSDAs to a Decidable Fragment of Strand

EQSDAs introduced in the previous section can express quantified data invariants over acyclic singly-linked data structures. In this section we show that
EQSDAs have a nice property that the quantified invariants expressed by them
fall in a decidable fragment of first order logic, in particular the decidable fragment of Strand. Hence, once the fix-point computation has converged, the
invariants expressed by the EQSDAs can be used to validate assertions in the
program using decision procedures. In fact, the automaton model for EQSDAs
was chosen keeping in mind the decidability of the invariants expressed by them.
Given an EQSDA A we would like to translate it to an equivalent formula I such that the set of heap skinny-trees accepted by A corresponds to
the program configurations which model I. Recall that for any k−skinny-tree
H accepted by an EQSDA, the number of branching nodes in H is bounded
by k. The invariants I expressed by an EQSDA are quantified formulas of
the form ∃b1 . . . bk .∀y1 . . . yℓ .ϕ such that, in any model satisfying I, the existential variables B = {b1 , . . . , bk } are always instantiated with the branching
nodes in I. The first step of the translation associates an existential variable
bi with every state of the automaton which has more than one child (and thus
18

represents a branching point). Then we enumerate all simple (loopless) paths
in the automaton starting from a leaf state, say qi , to a final state, say qf ,
and record the structural constraints over these linear segments, φif (B, P V, Y ),
which capture the relative positions (over relations next, next+ and next∗ ) of
the pointer/universal and branching variables with respect to each other and the
data formula annotated at the final state f (qf ). These structural constraints can
be constructed as described in [12]. After consdering every pair of such states,
the formula corresponding to an EQSDA can be expressed as
^
_

I = ∃b1 . . . bk .∀y1 . . . yℓ .
(∧i φif ⇒ f (qf )) ∧ ( ∧i φif )
f

f

A key property in the decidable fragment of Strand is that universal quantification is not permitted to be over elements that are only a bounded distance
away from each other. See [12] for a proof that the structural constraints φif are
such that I falls in the decidable fragment of Strand.

7

Experimental Evaluation

We implemented the abstract domain over QSDAs and EQSDAs presented in
this paper, and evaluated them on several list-manipulating programs. We now
first present the implementation details followed by our experimental results. Our
prototype implementation along with the experimental results and programs can
be found at http://web.engr.illinois.edu/~garg11/qsdas.html.
Implementation details. Given a program P we compute the abstract semantics of the program over the abstract domain QF el over EQSDAs. A program is
a sequence of statements as defined by the grammar in Figure 1. In addition to
those statements, a program is also annotated with a pre-condition and a bunch
of assertions. The pre-condition formulas belong to a fragment of Strand over
lists and can express quantified properties like sortedness of lists, etc. Given
a pre-condition formula ϕ, we construct the smallest EQSDA (with respect to
the partial-order defined on the QSDAs) which accepts all the heap skinny-trees
which satisfy ϕ. This EQSDA gives us an abstraction of the initial configurations of the program. Starting from these configurations we compute the abstract
semantics of the program over QF el . The assert statements in the program are
ignored during the fix-point computation. Once the convergence of the fix-point
has been achieved, the EQSDAs can be converted back into decidable Strand
formulas (as described in Section 6.1) and the Strand decision procedure can
be used for validating the assertions.
We recall that the abstract domain QF el is an abstraction of QF . So, as much
as possible, we want to compute the abstract semantics over the more concrete
domain out of the two, i.e. QF . Therefore, for every statement in the program
we apply the abstract transformer F ♯ (and not the more abstract Fel♯ ). The
intermediate semantic facts (QSDAs) in our analysis are thus not necessarily
19

elastic. However to ensure convergence of the analysis, the QSDAs at the header
of the loops are first abstracted to elastic QSDAs using αel before the join.
Our abstract domains are parameterized by a quantifier-free domain F over
the data formulas. In our experiments, we instantiate F with the octagon abstract domain [26] from the Apron library [19]. It is sufficient to capture the
pre/post-conditions and the invariants of all our programs.

Programs
init
add-head
add-tail
delete-head
delete-tail
max
clone
fold-clone
copy-Ge5
fold-split
concat
sorted-find
sorted-insert
bubble-sort
sorted-reverse
expressOS-lookup-prev
gslist-append
gslist-prepend
gslist-last
gslist-free
gslist-position
gslist-reverse
gslist-custom-find
gslist-nth
gslist-remove
gslist-remove-link
gslist-remove-all
gslist-insert-sorted

#PV #Y #DV
2
2
3
2
4
2
4
5
4
3
4
2
4
4
3
3
4
2
3
3
4
3
3
3
4
5
5
5

1
1
1
1
1
1
1
1
1
1
1
2
2
2
2
2
0
0
0
0
0
0
1
0
0
0
1
2

1
1
1
1
1
1
1
1
0
1
1
2
1
1
0
1
1
1
0
0
0
0
1
1
1
0
1
1

Property #Iter Max. size Time (s)
checked
of QSDA
Init, List
4
19
0.0
Init, List
11
0.1
Init, List
4
29
0.1
Init, List
10
0.0
Init, List
5
51
0.5
Max, List
4
19
0.1
Init, List
4
44
0.7
Init, List
5
57
3.2
Gek, List
9
53
2.6
Gek, List
4
33
0.3
Init, List
5
44
0.7
Sort, List
5
38
0.3
Sort, List
6
163
5.8
Sort, List 5/18
191
42.8
Sort, List
5
43
1.5
Sort, List
6
73
2.2
List
8
3
0.0
List
3
0.0
Last, List
3
7
0.0
Empty, List
1
3
0.0
List
3
13
0.0
List
3
5
0.0
Gek, List
4
29
0.1
List
3
7
0.0
List
4
10
0.0
List
4
16
0.0
Gek, List
5
51
0.6
Sort, List
6
279
27.4

Table 2: Experimental results. Property checked — List: the return pointer points to
a list; Init: the list is properly initialized with some key; Max: returned value is the
maximum of all data values in the list; Gek: the list (or some parts of the list) have
data values greater than or equal to a key k; Sort: the list is sorted; Last: returned
pointer is the last element of the list; Empty: the returned list is empty.

Experimental results We evaluate our abstract domain on a suite of listmanipulating programs (see Table 2). For every program we report the number
of pointer variables (PV), the number of universal variables (Y), the number
of data variables (DV) and the property being checked for the program. We
also report the number of iterations required for the fixed-point to converge, the
maximum size of the intermediate QSDAs and finally the time taken, in seconds,
to analyze the programs.
20

The names of the programs in Table 2 are descriptive, and we only describe
some of them. The program copy-Ge5 is from [6] and copies from a list only
those entries into a new list whose data value is greater than or equal to 5.
Similarly, the program fold-split [6] splits a list into two lists–one which has
only those entries whose data values are greater than or equal to a key k and the
other list with entries whose data value is less than k. The program expressOSlookup-prev is a method from the module cachePage in a verified-for-security
platform for mobile applications [22]. The module cachePage maintains a cache
of the recently used disc pages as a priority queue based on a sorted list. This
method returns the correct position in the cache at which a disc page could
be inserted. The programs in the second part of the table are various methods
adapted from the Glib list library which comes with the GTK+ toolkit and the
Gnome desktop environment. The program gslist-custom-find finds the first
node in the list with a data value greater or equal to k and gslist-remove-all
removes all elements from the list whose data value is greater or equal to k. The
programs gslist-insert-sorted and sorted-insert insert a key into a sorted
list.
All experiments were completed on an Intel Core i5 CPU at 2.4GHz with
6Gb of RAM. The number of iterations is left blank for programs which do not
have loops. bubble-sort program converges on a fix-point after 18 iterations
of the inner loop and 5 iterations of the outer loop. The size of the intermediate
QSDAs depends on the number of universal variables and the number of pointer
variables and largely governs the time taken for the analysis of the programs. For
all programs, our prototype implementation computes their abstract semantics
in reasonable time. Moreover we manually verified that the final EQSDAs in
all the programs were sufficient for proving them correct (this validity check for
assertions can be mechanized in the future). The results show that the abstract
domain we propose in this paper is reasonably efficient and powerful enough to
prove a large class of programs manipulating singly-linked list structures.

21

References
1. F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina. Lazy abstraction with interpolants for arrays. In N. Bjørner and A. Voronkov, editors,
LPAR, volume 7180 of Lecture Notes in Computer Science, pages 46–61. Springer,
2012.
2. R. Alur and P. Černý. Streaming transducers for algorithmic verification of singlepass list-processing programs. In Proceedings of the 38th annual ACM SIGPLANSIGACT symposium on Principles of programming languages, POPL ’11, pages
599–610, New York, NY, USA, 2011. ACM.
3. T. Ball and M. Sagiv, editors. Proceedings of the 38th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2011, Austin, TX,
USA, January 26-28, 2011. ACM, 2011.
4. J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O’Hearn, T. Wies, and
H. Yang. Shape analysis for composite data structures. In Damm and Hermanns
[10], pages 178–192.
5. J. Berdine, B. Cook, and S. Ishtiaq. Slayer: Memory safety for systems-level code.
In Gopalakrishnan and Qadeer [13], pages 178–183.
6. A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu. On inter-procedural analysis
of programs with lists and data. In M. W. Hall and D. A. Padua, editors, PLDI,
pages 578–589. ACM, 2011.
7. B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. In Necula and
Wadler [27], pages 247–260.
8. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for
static analysis of programs by construction or approximation of fixpoints. In R. M.
Graham, M. A. Harrison, and R. Sethi, editors, POPL, pages 238–252. ACM, 1977.
9. P. Cousot, R. Cousot, and F. Logozzo. A parametric segmentation functor for
fully automatic and scalable array content analysis. In Ball and Sagiv [3], pages
105–118.
10. W. Damm and H. Hermanns, editors. Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings,
volume 4590 of Lecture Notes in Computer Science. Springer, 2007.
11. D. Distefano, P. W. O’Hearn, and H. Yang. A local shape analysis based on
separation logic. In H. Hermanns and J. Palsberg, editors, TACAS, volume 3920
of Lecture Notes in Computer Science, pages 287–302. Springer, 2006.
12. P. Garg, C. Löding, P. Madhusudan, and D. Neider. Learning Universally Quantified Invariants of Linear Data Structures. In CAV, 2013. To Appear.
13. G. Gopalakrishnan and S. Qadeer, editors. Computer Aided Verification - 23rd
International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science. Springer, 2011.
14. D. Gopan, T. W. Reps, and S. Sagiv. A framework for numeric analysis of array
operations. In J. Palsberg and M. Abadi, editors, POPL, pages 338–350. ACM,
2005.
15. S. Gulwani, B. McCloskey, and A. Tiwari. Lifting abstract interpreters to quantified
logical domains. In Necula and Wadler [27], pages 235–246.
16. B. Guo, N. Vachharajani, and D. I. August. Shape analysis with inductive recursion
synthesis. In J. Ferrante and K. S. McKinley, editors, PLDI, pages 256–265. ACM,
2007.
17. P. Habermehl, L. Holı́k, A. Rogalewicz, J. Simácek, and T. Vojnar. Forest automata
for verification of heap manipulation. In Gopalakrishnan and Qadeer [13], pages
424–440.

22

18. N. Halbwachs and M. Péron. Discovering properties about arrays in simple programs. In R. Gupta and S. P. Amarasinghe, editors, PLDI, pages 339–348. ACM,
2008.
19. B. Jeannet and A. Miné. Apron: A library of numerical abstract domains for static
analysis. In A. Bouajjani and O. Maler, editors, CAV, volume 5643 of Lecture Notes
in Computer Science, pages 661–667. Springer, 2009.
20. R. Jhala and K. L. McMillan. Array abstractions from proofs. In Damm and
Hermanns [10], pages 193–206.
21. P. Madhusudan, G. Parlato, and X. Qiu. Decidable logics combining heap structures and data. In Ball and Sagiv [3], pages 611–622.
22. H. Mai, E. Pek, H. Xue, S. T. King, and P. Madhusudan. Verifying security
invariants in ExpressOS. In V. Sarkar and R. Bodı́k, editors, ASPLOS, pages
293–304. ACM, 2013.
23. R. Manevich, E. Yahav, G. Ramalingam, and S. Sagiv. Predicate abstraction and
canonical abstraction for singly-linked lists. In R. Cousot, editor, VMCAI, volume
3385 of Lecture Notes in Computer Science, pages 181–198. Springer, 2005.
24. B. McCloskey, T. W. Reps, and M. Sagiv. Statically inferring complex heap, array,
and numeric invariants. In R. Cousot and M. Martel, editors, SAS, volume 6337
of Lecture Notes in Computer Science, pages 71–99. Springer, 2010.
25. K. L. McMillan. Quantified invariant generation using an interpolating saturation
prover. In C. R. Ramakrishnan and J. Rehof, editors, TACAS, volume 4963 of
Lecture Notes in Computer Science, pages 413–427. Springer, 2008.
26. A. Miné. The octagon abstract domain. In WCRE, pages 310–, 2001.
27. G. C. Necula and P. Wadler, editors. Proceedings of the 35th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2008, San
Francisco, California, USA, January 7-12, 2008. ACM, 2008.
28. A. Podelski and T. Wies. Counterexample-guided focus. In M. V. Hermenegildo
and J. Palsberg, editors, POPL, pages 249–260. ACM, 2010.
29. S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued
logic. ACM Trans. Program. Lang. Syst., 24(3):217–298, 2002.
30. M. N. Seghir, A. Podelski, and T. Wies. Abstraction refinement for quantified
array assertions. In J. Palsberg and Z. Su, editors, SAS, volume 5673 of Lecture
Notes in Computer Science, pages 3–18. Springer, 2009.

23

A

Formal Semantics of Programs

In this appendix we describe the concrete semantics of the primitive statements
in our programming language defined in Figure 1. Let us assume that there is
a special program configuration Error to which the progam transitions to on
encountering a memory error.
Definition 3 (Strongest post-condition F ♮ ). Let C = (pc, H, pval, dval) be
a non-Error program configuration where H = (Loc, next, data). Then for
any statement s, C ′ is the strongest post-condition of C with respect to the
s
statement s, written as C −
→P C ′ , iff C ′ = (pc′ , H ′ , pval′ , dval′ ) where H ′ =
(Loc′ , next′ , data′ ) and pc′ is the updated program counter and one of the following holds:
– s = pi := pj (or s = pi := nil) and H ′ = H and dval′ = dval and pval′ =
pval[pi /pval(pj )] (or pval′ = pval[pi /pval(nil)]).
– s = pi := pj → next and H ′ = H and dval′ = dval and if pval(pj ) = v and
(v, u) ∈ next, then pval′ = pval[pi /u]. If v = dirty or v = nil, then C ′ is
Error.
– s = pi → next := pj (or s = pi → next := nil) and pval′ = pval and
dval′ = dval and Loc′ = Loc and data′ = data and if pval(pi ) = v
and (v, u) ∈ next and if pval(pj ) = w (or pval(nil) = w), then next′ =
next\{(v, u)} ∪ {(v, w)}. If v = nil or v = dirty, then C ′ is Error.
– s = new pi and dval′ = dval and Loc ′ = Loc ∪ {v}, v ∈
/ Loc, next′ =
′
′
next ∪ {(v, dirty)} and data = data and pval = pval[pi /v].
– s = di := pi → data and H ′ = H and pval′ = pval and if pval(pi ) = v, then
dval′ = dval[di /data(v)]. If v = nil or v = dirty then C ′ is Error.
– s = pi → data := data expr and pval′ = pval and dval′ = dval and Loc′ =
Loc and next′ = next and if pval(pi ) = v then data′ = data[v/data expr].
If v = nil or if v = dirty then C ′ is Error.
– s = skip and C ′ = C.
– s = assume (ψstruct ) and C ′ = C and C |= ψstruct .
– s = assume (ψdata ) and C ′ = C and C |= ψdata .

B

Proof of Theorem 6

Note that Ael is elastic by definition of ∆el
1 . It is also clear that Lv (A) ⊆ Lv (Ael )
because for each run of A using states q0 · · · qn the run of Ael on the same input
uses sets S0 · · · Sn such that qi ∈ Si , and by definition f (qn ) implies f el (Sn ).
Now let B be an EQSDA with Lv (A) ⊆ Lv (B). Let t be a valuation tree
accepted by Ael and let S be the state of Ael reached on reading t. We want to
show that t ∈ Lv (B). Let p be the state reached in B on t. We show that f (q)
implies fB (p) for each q ∈ S. From this we obtain f el (S) ⇒ fB (p) because f el (S)
is the least formula that is implied by all the f (q) for q ∈ S.
Pick some state q ∈ S. By definition of ∆el we can construct a valuation tree
′
t ∈ Lv (A) that leads to the state q in A and has the following property: if all
24

letters of the form (b, d) and those that have a single child are removed from t
and from t′ , then the two remaining trees have the same symbolic trees. In other
words, t and t′ can be obtained from each other by inserting and/or removing
b-letters.
Since B is elastic, t′ also leads to p in B. From this we can conclude that
f (q) ⇒ f (p) because otherwise there would be a model of f (q) that is not
a model of f (p) and by changing the data values in t′ accordingly we could
produce an input that is accepted by A and not by B.
⊓
⊔

C

Construction of the Strengthen Operator

Given a QSDA A, we give below a high level sketch of how to construct the QSDA
A′ accepting the following language of formula words: (Strengthen) y Lf (A).
The construction of the QSDA A′ takes place in two steps.
In the first step, we construct a QSDA
A1 which

daccepts (Σ ×(Y ∪{−}\{y}))labelled formula trees of the form (t′ ⇂y , φ) | φ : {∃d.ϕ[y → data/d] | (t, ϕ) ∈
Lf (A), t ⇂y = t′ ⇂y } .
And in the second step, we take the cross-product of this automaton A1
with the initial automaton A to get the QSDA A′ such that if the symbolic tree
t′ ⇂y is mapped by A1 to data-formula φ and the symbolic tree t′ is mapped
by A to the data-formula ϕ′′ , then t′ is mapped in the new automata A′ to
the data-formula φ ⊓ ϕ′′ . The required cross-product of two QSDAs is similar to
the algorithm for computing intersection of tree automata. The automata which
computes the cross-product simulates the transitions of both the automata A
and A1 . However, since A1 accepts trees which do not have the variable y labeling
them, the cross-product automata on a label π which contains y simulates the
transitions of A on the label π, but simulates the transition of A1 on the label
π\{y}. The states in the cross-product automaton are labeled with the meet of
the data-formulas labeling the states of the two individual automata.
So now let us describe the construction of the automaton A1 . The QSDA
A1 accepts symbolic trees of the form t ⇂y if (t, ϕ) ∈ Lf (A). Hence, A1 is an
automaton which simulates the transitions of A on a symbolic tree, except when
it reads a node in the tree labeled with label π which contains variable y. When
this happens, A1 simulates the transitions of A on the label π\{y}. The dataformulas mapped to each state in A1 is obtained by existentially quantifying
out y → data from the data-formulas mapping the corresponding states in
A. Note that the transition relation of A1 we just described might be nondeterministic; the same symbolic tree t ⇂y might be mapped to more than one
data-formula eg. ∃d.ϕ1 [y → data/d] and ∃d.ϕ2 [y → data/d] and so on. We
want the automata A1 to map t ⇂y to the meet of all these formulas. This can be
achieved by determinizing the transition relation of the QSDA, very similar to
the determinization procedure of a tree automata. In addition, for a set of states
in the deterministic automata, we label it with the meet of the data-formulas
labeling each state in the set in the original non-deterministic automata. In this
25

way, the transition relation could be determinized to obtain QSDA A1 . This
completes the construction of A′ .

D

Construction of the Abstract Transformer

First let us introduce some preliminary notation. For a set S, let S i denote the
ith cartesian power of S. For an n-tuple x = (x1 , . . . , xn ) ∈ X = X1 × . . . × Xn ,
let us define x ↓i for 1 ≤ i ≤ n as the projection onto the ith component of the
tuple i.e. (x1 , . . . , xn ) ↓i = xi . When the set Xi can be uniquely distinguished
from all other components Xj of the n-tuple X, x ↓Xi = xi is also used to denote
the Xith component of the tuple x. For a tuple x, x′ = x[X1 /x1 , . . . , Xk /xk ] is
used to denote the tuple which is same as x except at the X1 , . . . , Xk components
where the tuple x′ takes the value x1 , . . . , xk respectively.
For a function F : D → X, where X = X1 × . . . × Xn , which maps a domain
D to an n-tuple X, let F ↓i : D → Xi for 1 ≤ i ≤ n be defined such that
F ↓i (d) = F (d) ↓i for all d ∈ D. Also for a function f , let us denote f |D as
the function which is same as f but with its domain restricted to the set D. for
a given function f , let us also define f ′ = f [d1 /v1 , . . . , dk /vk ] as the function
which is same as f except at the domain elements d1 , . . . , dk where f ′ takes the
value v1 , . . . , vk .
We now present the construction of the abstract transformer for each case of
the statement stmt. Let the input QSDA be of the form (Q, Π, ∆, T , f ) where
Π = (Σ × (Y ∪ {−})) and Σ = 2P V . Let us view Σ as a set of boolean vectors where the ith bit in a vector indicates whether the pointer pi belongs to
the vector or not. The output QSDA after the execution of stmt is of the form
(Q′ , Π, ∆′ , T ′ , f ′ ) where:
Case 1 (s = pi := pj ): The evaluation function f ′ of the automaton depends on
whether pj co-occurs with nil or not. To facilitate this, we split each state into
two states Q′ = Q ∪ {(q, nil) | q ∈ Q)}. Regarding the transition relation, for all
transitions ∆(q1 , .., qp , π) = q,
– if pj 6∈ T (q), ∆′ (q1 , .., qp , π[pi /0]) = q.
– if pj ∈ T (q) and π ↓pj = 1 and π ↓pnil = 1, then ∆′ (q1 , .., qp , π[pi /1]) =
(q, nil)).
– if pj ∈ T (q) and π ↓pj = 1 and π ↓pnil = 0, then ∆′ (q1 , .., qp , π[pi /1]) = q.
– if pj ∈ T (q) and π ↓pj = 0 then there exists a state qj , 1 ≤ j ≤ p such that
pj ∈ T (qj ). Correspondingly, we add transitions ∆′ (q1 , ..., qj , ..., qp , π[pi /0])
= q and ∆′ (q1 , ..., (qj , nil), ..., qp , π[pi /0]) = (q, nil).
′
The type T ′ for every
state ∈ Q is:

/ T (q)
T (q) ∪ {pi } if pj ∈ T (q), pi ∈
T ′ (q) = T ′ (q, nil) = T (q)\{pi }
if pj ∈
/ T (q), pi ∈ T (q)


T (q)
otherwise
The evaluation function depends on whether the pointer pj is nil or not. Hence,

26

f ′ (q) = ∃d.f (q)[pi → data/d]⊓(pi → data = pj → data). Otherwise, f ′ (q, nil) =
∃d.f (q)[pi → data/d].
Case 2 (s = pi := pm → next): Firstly, Q′ = {q | q ∈ Q, pm ∈
/ T (q)} ∪
{(q, ∗), (q, v) | q ∈ Q, pm ∈ T (q), v ∈ P V ∪ Y ∪ {−}}. The automaton transitions to a state of the form (q, ∗) on reading the pointer variable pm . This is
like guessing the state in which the automaton transitions to, on reading variable pm . After reading pm , the automaton reads variable pi and transitions from
state (q, ∗) to a state of the form (q ′ , v) where v is basically a pointer variable or
a universal variable which is co-read with pi . The variable v is used later when
defining the evaluation functions for states Q′ .
More formally, for all transitions ∆(q1 , ..., qp , π) = q,
– if pm ∈
/ T (q) then ∆′ (q1 , ..., qp , π[pi /0]) = q.
– if pm ∈ T (q) and π ↓pm = 1 then ∆′ (q1 , ..., qp , π[pi /0]) = (q, ∗).
– if pm ∈ T (q) and π ↓pm = 0 then there exists a state qm ∈ {q1 , ..., qp } such
that pm ∈ T (qm ). Accordingly we add the transition, ∆′ (q1 , ..., (qm , ∗), ..., qp ,
π[pi /1]) = (q, v) if there exists a variable v ∈ P V ∪ Y such that π ↓v = 1 and
π ↓nil = 0. Otherwise the transition ∆′ (q1 , ..., (qm , ∗), ..., qp , π[pi /1]) = (q, −).
This covers the case when state qm was reached immediately after reading
variable pm . For the other case, we add transitions ∆′ (q1 , ..., (qm , v) , ..., qp
, π[pi /0]) = (q, v) for all v ∈ P V ∪ Y ∪ {−}.
Note that the final evaluation formula is only associated with states of the
form (q, v) or (q, −). For all q ∈ Q such that pm ∈ T (q) and v ∈ P V ∪ Y ,
f ′ (q, v) = ∃d.f (q)[pi → data/d] ⊓ (pi → data = v → data). Otherwise,
f ′ (q, −) = ∃d.f (q)[pi → data/d]. For all other states, the evaluation formula
is f alse.
′
′
′
Finally,
 for all q ∈ Q , the type associated with q is given as:
′
′
′

/ T (q )
T (q )\{pi } if q ∈ Q, pm ∈
T ′ (q ′ ) = T (q)\{pi }
if q ′ = (q, ∗), q ∈ Q


T (q) ∪ {pi } if q ′ = (q, v), q ∈ Q, v ∈ P V ∪ Y ∪ {−}
Case 3 (s = new pi ): The statement s allocates a new node which is pointed
to by variable pi and is added as a child to the root of data trees accepted by
the original automaton. The universal variables, apart from the nodes already
present in the data trees, now also have to valuate over the newly allocated
node. The set of states of the new automaton is Q′ = (Q ∪ {q̂}) × Ŷ where
q̂ ∈
/ Q. The states of the form (Q ∪ {q̂}, y) are used to accept valuation trees
where univeral variable y valuates over the newly allocated node whereas the
other universal variables valuate over the existing nodes present in the heap
tree. The states (Q ∪ {q̂}, −) are used to accept valuation trees where none of
the universal variable valuates to the newly allocated node. The state q̂ is used
to transition the automaton to a special state on reading the new node labeled
with pointer variable pi i.e. ∆′ (({pi }, ŷ)) = (q̂, ŷ) for all ŷ ∈ Ŷ . Also for all
transitions ∆(q1 , ..., qp , π) = q,
27

– if π ↓root = 0, ∆′ ((q1 , ŷ), ..., (qp , ŷ), π[pi /0, ŷ/0]) = (q, ŷ) for all ŷ ∈ Ŷ .
– if π ↓root = 1, ∆′ ((q1 , ŷ), ..., (qp , ŷ), (q̂, ŷ), π[pi /0, ŷ/0]) = (q, ŷ) for all ŷ ∈ Ŷ .
The final
 evaluation formula is given as:
∃d1 d2 .f (q)[pi → data/d1 , y → data/d2 ] ⊓ (pi → data = y → data)




if q ∈ Q, ŷ = y ∈ Y
f ′ (q, ŷ) =

∃d.f
(q)[p
→
data/d]
if
q ∈ Q, ŷ = −
i



false
if q = q̂

Also thetypes for each

{pi }





{p
 i , y}
′
T (q, ŷ) = T (q)\{pi }



T (q)\{pi , y}



T (q)

state in the new automaton are:
if q = q̂, ŷ = −
if q = q̂, ŷ = y ∈ Y
if q ∈ Q, root ∈
/ T (q), ŷ = −
if q ∈ Q, root ∈
/ T (q), ŷ = y ∈ Y
if q ∈ Q, root ∈ T (q)

Case 4 (s = pm → next := pi ): Firstly, Q′ = Q ∪ (Q, ∗) ∪ {(q1 , q2 ) | q1 , q2 ∈
Q, pi ∈ T (q1 ) iff pm ∈
/ T (q1 )}. From the semantics of the strongest-post, we
know that the new automaton removes any sub-tree rooted at pm and attaches
it as an additional child to a node labelled with variable pi . States of the form
(Q, ∗) are special states in which the automaton transitions to on reading the
variable pm . If (q2 , ∗) accepts a tree τm rooted at pm then the state (q1 , q2 )
where pi ∈ T (q1 ) accepts a tree which has τm as an additional child to an internal node labelled with pi . On the other hand, if pm ∈ T (q1 ) then (q1 , q2 )
accepts a tree which had its subtree τm , rooted at pm , removed. Describing the
transition relation in detail, for a transition ∆(q1 , ..., qp , π) = q:
1. if {pi , pm }∩T (q) = φ, then we add the same transition to the new automaton
i.e. ∆′ (q1 , ..., qp , π) = q.
2. if pm ∈ T (q) and pi ∈
/ T (q)
– and if π ↓pm = 1 then the automaton should transition to a state of the
form (Q, ∗); therefore ∆′ (q1 , ..., qp , π) = (q, ∗).
– otherwise, there exists a state qm ∈ {q1 , ..., qp } such that pm ∈ T (qm ). In
case qm , in the original automaton, accepted trees rooted at pm , the new
automaton should remove qm from the left hand side of the transition
and should transition to a state (q, qm ) via ∆′ (q1 , .., qm−1 , qm+1 , ...,
qp , π) = (q, qm ). To handle the other case, where qm accepted trees which
were not rooted at pm , the transitions ∆′ (q1 , ..., (qm , q̂), ..., qp , π) = (q, q̂)
are added for all q̂ ∈ Q.
3. if pi ∈ T (q) and pm ∈
/ T (q)
– and if π ↓pi = 1 then the new automaton should accept a tree at q which
has an additional child τm rooted at pm . Since all trees rooted at pm
are accepted at states of the form (Q, ∗) (the first subcase of 2 above),
transition ∆′ (q1 , ..., qp , (qm , ∗), π) = (q, qm ) is added for all qm ∈ Q.
28

– otherwise, there exists a state qi ∈ {q1 , ..., qp } such that pi ∈ T (qi ) and
the fact, that any node labelled with pi in the tree accepted at q has as
an additional child a tree τm rooted at pm , is propagated recursively via
the transitions ∆′ (q1 , ..., (qi , qm ), ..., qp , π) = (q, qm ) for all qm ∈ Q.
4. if {pi , pm } ⊆ T (q)
– and π ↓pm = 1 (reagrdless of the value of π ↓pi ) no transition is added
to ∆′ , as any heap configuration accepted by the original automaton via
this transition leads to a cycle on the execution of statement stmt.
– otherwise if π ↓pm = 0 and π ↓pi = 1, there will exist a state qm ∈
{q1 , ..., qp } such that pm ∈ T (qm ). The corresponding state in the new
transition will be (qm , q̂) if q̂ was the state of the original automaton
which accepted the internal subtree τm rooted at pm . Since π ↓pi = 1,
an additional state (q̂, ∗) is added to the left hand side of the transition
to ensure that the new automaton accepts the tree which has τm as an
additional child to a node labelled with pi . Formally, ∆′ (q1 , ..., (qm , q̂),
..., qp , (q̂, ∗), π) = q for all q̂ ∈ Q.
– otherwise if π ↓pm = π ↓pi = 0 and there exists a state qim ∈ {q1 , ..., qp }
such that {pi , pm } ⊆ T (qim ) then the transition remains unchanged i.e.
∆′ (q1 , ..., qim , ..., qp , π) = q.
– otherwise if π ↓pm = π ↓pi = 0 and there exist states qi , qm ∈ {q1 , ..., qp }
such that pi ∈ T (qi ) and pm ∈ T (qm ), then the transition ∆′ (q1 , ...,
(qi , q̂), ..., (qm , q̂), ..., qp , π) = q is added for all q̂ ∈ Q. Note that (qi , q̂)
accepts a tree which has an additional child (accepted at (q̂, ∗)) at a
node labelled with pi (explained in case 3 above) and (qm , q̂) accepts a
tree where the internal subtree rooted at pm and accepted at (q̂, ∗) has
been removed (explained in the second subcase of 2 above). Note that if
qm = q̂ then the state (qm , q̂) is removed from the left hand side of the
transition ∆′ i.e. ∆′ (q1 , ..., (qi , q̂), ..., qp , π) = q.
The final evaluation formula is unchanged for the states Q ⊆ Q′ , it is false
for the newly added states i.e. f ′ (q) = f (q), q ∈ Q and f ′ (q, ∗) = f ′ (q1 , q2 ) =
′
false. The
 type T for the new automaton is defined as:
T (q)
if q ∈ Q



T (q̂)
if q = (q̂, ∗), q̂ ∈ Q
T ′ (q) =

T
(q
)
∪
T
(q
)
if q = (q1 , q2 ), pi ∈ T (q1 )
1
2



T (q1 )\T (q2 )
if q = (q1 , q2 ), pm ∈ T (q1 )
Case 5 (s = pm → data := a): On execution of this statement, the structure component of the data trees accepted by the automaton is unchanged;
however the final evaluation function has to now record the fact that the value
of the data pointed by variable pm is assigned the value of a. If, for a particular valuation tree, pm is co-read with variable v ∈ P V ∪ Y before it is
accepted at state q, f ′ (q) should also record that the data value pointed by
variable v is now assigned to a. So the new automaton needs to track the set
of variables which are co-read with pm for a particular valuation tree. Hence
29

Q′ = {q | q ∈ Q, pm ∈
/ T (q)} ∪ {(q, S) | q ∈ Q, pm ∈ T (q), S ⊆ P V ∪ Y }.
Regarding the transition relation, for all transitions ∆(q1 , ..., qp , π) = q,
– if pm ∈
/ T (q), ∆′ (q1 , ..., qp , π) = q.
– otherwise if pm ∈ T (q)
• and if π ↓pm = 1 then ∆′ (q1 , ..., qp , π) = (q, S) where ∀s ∈ S. π ↓s = 1.
• otherwise if π ↓pm = 0 then there exists a state qm ∈ {q1 , ..., qp } such that
pm ∈ T (qm ). Consequently, we add transitions ∆′ (q1 , ..., (qm , S), ..., qp , π) =
(q, S) for all S ⊆ P V ∪ Y .
The final evaluation function f ′ is given as: f ′ (q) = f (q) for all q ∈ Q ∩ Q′ ;
f (q, S) = ∃d.f (q)[v1 → data/d, . . . , vℓ → data/d]⊓(v1 → data = a)⊓. . .⊓(vℓ →
data = a) where S = {v1 , ..., vℓ } and includes variable pm . The type for each
state of the new automaton is also same as the type in the original automaton
i.e. T ′ (q) = T (q) for all q ∈ Q ∩ Q′ ; while T (q, S) = T (q) for all S in the remaining states.
′

Case 6 (s = assume (pi = pj ) ): The output QSDA is obtained by removing from
the input QSDA, transitions where variables pi and pj do not occur together.
Formally, Q′ = Q, f ′ = f, T ′ = T and for all transitions ∆(q1 , ..., qp , π) = q in
the input QSDA, ∆′ (q1 , ..., qp , π) = q iff π ↓pi = π ↓pj .
Case 7 (s = assume (pi 6= pj ) ): The output QSDA is obtained by removing from the input QSDA, transitions where variables pi and pj occur together.
Formally, Q′ = Q, f ′ = f, T ′ = T and for all transitions ∆′ (q1 , ..., qp , π) = q in
the input QSDA, ∆′ (q1 , ..., qp , π) = q iff π ↓pi = 0 or π ↓pj = 0 or both.
Case 8 (s = assume ψdata ): In this case, Q′ = Q and the transitions ∆′ is
same as ∆. The type T ′ = T and for all q ∈ Q, f ′ (q) = f (q) ⊓ ψdata .
The transition relation ∆′ thus constructed might need to be determinized to obtain A′ . For a symbolic tree t and formulas ϕ1 , . . . , ϕj such that (t, ϕ1 ), . . . , (t, ϕj )
belong to the language, the determinization procedure maps t to the formula
ϕ1 ⊔ . . . ⊔ ϕj . The determinization procedure is similar to the powerset construction for determinizing tree automata; except for any set of states, the final
evaluation function is now assigned to be the join of the formulas being mapped
to the individual states in the set.

30

