Automatically Refining Partial Specificationsfor Heap-Manipulating Programs
Shengchao Qina , Guanhua Hea , Chenguang Luoa , Wei-Ngan Chinc , Hongli Yangba School of Computing, Teesside University
b College of Computer Science, Beijing University of Technologyc School of Computing, National University of Singapore

Abstract
Automatically verifying heap-manipulating programs is a challenging task, especially when dealing withcomplex data structures with strong invariants, such as sorted lists and AVL/red-black trees. The verification
process can greatly benefit from human assistance through specification annotations, but this process requires
intellectual effort from users and is error-prone. In this paper, we propose a new approach to program
verification that allows users to provide only partial specification to methods. Our approach will then refine
the given annotation into a more complete specification by discovering missing constraints. The discovered
constraints may involve both numerical and multi-set properties that could be later confirmed or revisedby users. We further augment our approach by requiring partial specification to be given only for primarymethods. Specifications for loops and auxiliary methods can then be systematically discovered by ouraugmented mechanism, with the help of information propagated from the primary methods. Our work is
aimed at verifying beyond shape properties, with the eventual goal of analysing full functional properties forpointer-based data structures. Initial experiments have confirmed that we can automatically refine partial
specifications with non-trivial constraints, thus making it easier for users to handle specifications with richer
properties.
Keywords: static program analysis, separation logic, numerical analysis, partial specification refinement,semi-automatic software verification, constraint abstraction
PACS: 07.05.Bx, 89.20.Ff

Contents
1 Introduction

2

2 The Approach
2.1 The Hip/Sleek System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2 An Illustrative Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2.1 Analysis for the Unannotated Method . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 Another Illustrative Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3.1 Analysis for the while loop. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4
4
5
7
7
9

3 Language and Abstract Domain

10✩ This is an extended version of an FM2011 paper.
✩✩ This research was supported in part by EPSRC Project EP/G042322.

Email addresses: shengchao.qin@gmail.com (Shengchao Qin), g.he@tees.ac.uk (Guanhua He), chinwn@comp.nus.edu.sg(Wei-Ngan Chin), yhl.yang@gmail.com (Hongli Yang)

Preprint submitted to Elsevier

April 6, 2013

4 The Analysis
4.1 Refining Specifications for Primary Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Pure abduction mechanism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Inferring Specifications for Auxiliary Methods and Loops . . . . . . . . . . . . . . . . . . . .
4.4 Symbolic Execution Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.5 Soundness and Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

11
12
14
15
16
19

5 Experiments and Evaluation

20

6 Related Work and Conclusion
22
6.1 Related works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
6.2 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
Appendix A

Shape Predicate Definitions

26

1. Introduction
Human assistance is often essential in (semi-) automated program verification. The user may supply
annotations at certain program points, such as loop invariants and/or method specifications. These annotations can greatly narrow down the possible program states at that point, and avoid fixed-point calculation
which could be expensive and may be less precise than the user’s insight.
However, an obvious disadvantage of user annotation concerns its scalability, since programs to beanalysed may be complicated and with significant diversity. Therefore, it may be unreasonable to expect
users to provide specifications for every method and invariants for every loop when verifying larger softwaresystems. Furthermore, to err is human. A programmer may under-specify with too weak a precondition or
over-specify with too strong a postcondition. Such mistakes could lead to failed verification, and it may bedifficult for the user to distinguish whether a failure is due to a real bug in the program or an inappropriately
supplied annotation.
To balance verification quality and human effort, we provide a novel approach to the verification of heap
manipulating programs, which has long been a challenging problem. To deal with such programs, which
manipulate heap-allocated shared mutable data structures, one needs to keep track of not only “shape”
information (for deep heap properties) but also related “pure” properties, such as structural size information(length and height), relational numerical information (balanced and sortedness properties), and content
information (multi-set of symbolic values). Under our framework, the user is expected to provide partial
specifications for primary methods with only shape information. Our verification will then take over the restof the work to refine those partial specifications with derived (pure) constraints which should be satisfied by
the program, or report a potential program bug if the given specifications are rejected by our verifier. Thisis an improvement over previous works [1, 2] where users must provide full specifications for each method
and invariants for each loop. This is also significantly different from compositional shape analysis [3, 4, 5].
In spite of a higher level of automation, their analysis focuses on pointer safety only and deals primarily witha few built-in predicates over the shape domain only. Our work targets both memory safety and functionalcorrectness and supports user-defined predicates over several abstract domains (such as shape, numerical,
multi-set).
Our approach allows the user to design their predicates for shapes and relative properties, to capture
the desired level of program correctness to be verified. For example, with a singly-linked list structure
data node { int val; node next; }, a user interested in pointer-safety may define a list shape predicate (asin [3, 4]):list(root) ≡ (root=null)∨(∃i, q · root7→node(i, q)∗list(q))
Note that in the inductive case, the separation conjunction ∗ ([6]) ensures that two heap portions (the headnode and the tail list) are domain-disjoint. The parameter root for the predicate is the root pointer referringto the data structure.
2

Yet another user may be interested to track also the length of a list to analyse quantitative measures,usingll(root, n) ≡ (root=null∧n=0)∨(root7→node( , q)∗ll(q, m)∧n=m+1)
Note that unbound variables, such as q and m, are implicitly existentially quantified, and is used to denote
an existentially quantified anonymous variable. This predicate may be extended to capture the content
information, to support a higher level of correctness with a multi-set (bag) property:llB(root, S)≡(root=null∧S=∅)∨(root7→node(v, q)∗llB(q, S1 )∧S={v}⊔S1 )where the length of the list is implicitly captured by the cardinality |S|. The operator ⊔ is for bag union. A
further strengthening can capture also the sortedness property:sllB(root, S)≡(root=null∧S=∅)∨(root7→node(v, q)∗sllB(q, S1 )∧S={v}⊔S1 ∧(∀x∈S1 ·v≤x))
Therefore, users can provide predicate definitions with respect to various correctness level and program
properties, which can be as simple as normal lists or as complicated as AVL trees, depending on theirrequirements. These predicates are non-trivial to be defined but can be reused multiple times for specifications of different methods. Hence efforts involved in such predicate design are often significantly amortised.
We have built a library of predicates with respect to commonly-used data structures and useful program
properties.
Based on these predicates, the user is expected to provide partial specifications for some primary methods
which are the main objects of verification. For example, a sorting algorithm taking x as input parameter thatis expected to be non-null. The user may provide llB(x, S1 ) as precondition and sllB(x, S2 ) as postcondition.
Our approach will refine the specification as llB(x, S1 )∧x6=null for precondition, and sllB(x, S2 )∧S1 =S2 forpostcondition. Here we need user annotations as the initial specification, because we reserve the flexibilityof verification with respect to different program properties at various correctness levels. For instance, ourapproach can verify the same algorithm, but for different refined specifications, such as:
requires list(x)requires ll(x, n1 )requires llB(x, S1 )∧ x6=null∧ n1 >0∧ x6=null

ensures
ensures
ensureslist(x)ll(x, n2 )∧ n1 =n2llB(x, S2 ) ∧ S1 =S2

requires llB(x, S)∧ x6=null

ensuresll(x, n)∧ |S|=nwhere the discovered missing constraints are shown in shaded form.
To summarise, our proposal for refining partial specification is aimed at harnessing the synergy between ahuman’s insights and a machine’s capability at automated program analysis. In particular, human guidance
can help narrow down on the most important of the different specifications that are possible with eachprogram code, while automation by machine is important for minimising on the tedium faced by users. Our
proposal has the following characteristics:• Specification completion: We discover three types of constraints added into the user-given incomplete
specification: constraints in the precondition for memory safety, (relational) constraints in postcondition to link the method’s pre- and post-states, and constraints that the method’s post-state satisfies.
• Flexibility: We allow the user to define their own predicates for the program properties they want toverify, so as to provide different levels of correctness. Meanwhile we aim at, and have covered muchof, full functional correctness of pointer-manipulating programs such as data structure shapes, pointersafety, structural/relational numerical constraints, and bag information.
• Reduction of user annotations: Our approach uses program analysis techniques effectively to reduceusers’ annotations. As for our experiments, the user only has to supply the partial specifications
for primary methods, and the analysis will compute pre- and postconditions for loops and auxiliary
methods as well as refine primary methods’ specifications.
3• Semi-Automation: We classify our approach as semi-automatic, because the user is allowed to interveneand guide the verification at any point. For instance, they may provide invariant for a loop insteadof our automated invariant generation, or choose some other constraints as refinement from what theverification has discovered.
We have built a prototype implementation and carried out a number of experiments to confirm theviability of the approach as described in Section 5. In what follows, we will first depict our approach
informally using two motivating examples and present technical details thereafter. More related works andconcluding remarks come after the experimental results.
2. The Approach
In this section, we briefly introduce the Hip/Sleek system as the base of our verification and refinement.
We then use some motivating examples to informally illustrate our approach.
2.1. The Hip/Sleek System
Separation logic [7, 6] extends Hoare logic to support reasoning about shared mutable data structures.
One connective that it adds to classical logic is separation conjunction ∗. The separation formula p1 ∗p2means that the heap can be split into two disjoint parts in which p1 and p2 hold respectively. Our work will
make use of this connective in our specifications.
For better flexibility and expressivity, Hip/Sleek allows users to define inductive shape predicates toleverage both shape and pure properties. We have illustrated several of these shape predicate definitions in
the last section. For more involved examples, based on a data structure definition data node2 { int val;
node2 prev; node2 next; }, one may define the predicate below to specify sorted doubly-linked list segments:
sdlB(root,p, q, S) ≡(root=q ∧ S=∅) ∨(root7→node2(v, p, t)∗sdlB(t,root, q, S1 )∧root6=q∧S={v}⊔S1 ∧(∀x∈S1 ·v≤x))where the parameters p and q denote the prev field of root and the next field of the last node in the list
respectively. Meanwhile S is a bag (multi-set) parameter to represent the list’s content. We can see in thebase case of definition that S=∅, and in the recursive case that all values stored after root must be no lessthan root’s value.
Another example is the definition of node-balanced trees with binary search property:
nbt(root,S) ≡(root=null ∧ S=∅) ∨(root7→node2(v, p, q)∗nbt(p,Sp )∗nbt(q,Sq ) ∧ S={v} ⊔ Sp ⊔ Sq ∧(∀x∈Sp ·x≤v) ∧ (∀x∈Sq ·v≤x) ∧ −1≤|Sp |−|Sq |≤1)
where S captures the content of the tree. We require the difference in node numbers of the left and rightsub-trees be within one, as the node-balanced property indicates.
User-defined predicates may then be used to specify loop invariants and method pre/post-specifications.
In Hip/Sleek , the Hip verifier is used to automatically verify programs against their specifications, while
the Sleek prover is invoked by the verifier to conduct entailment proofs. Given two separation formulas∆1 and ∆2 , Sleek attempts to prove that ∆1 entails ∆2 ; if it succeeds, it returns a frame ∆R such that
∆1 ⊢ ∆2 ∗∆R . For instance, given the entailment queryll(p,n) ∧ n>0 ⊢ ∃q · node(p,q) ∗ [∆R ]Sleek produces the following result after unfolding the LHS predicate:ll(p,n) ∧ n>0 ⊢ ∃q · node(p,q)∗[ll(q,n−1) ∧ n>0]
where the inferred frame is shown in square brackets as the residue of the entailment check. The proposed
analysis in this paper will use Sleek to perform deductions of separation formulas.
4

2.2. An Illustrative Example
We firstly illustrate our approach using method insert sort in Fig. 1. We show how our analysis infers
missing constraints to improve the user-supplied incomplete specification, and how it analyses auxiliary
methods without user-annotations.

1 data node { int val; node next; }11 node insert(node r, node x) {2 node insert_sort(node x)

123

requires llB(x,S)

13

x.next = null; return x;

4ensures sllB(res,T)

14} else if (x.val <= r.val) {5 { if (x.next == null) return x;

15

6

16

else { node s = x.next;

if (r == null) {x.next = r; return x;} else {7

node r = insert_sort(s);17r.next = insert(r.next, x);

8

return insert(r, x);18

return r;

9

19

}

}

20 }

10 }

Figure 1: The insertion sort program for lists.

The insert sort method sorts a singly-linked list. It takes in an unsorted list starting from x with content
S and returns a sorted list (as indicated by the specifications in lines 3 and 4 where res denotes the method
return value). The algorithm first sorts the list referenced by x.next recursively (line 7), and then inserts
node x into the resulted sorted list (line 8). For the node insertion, it invokes another method insert for
which the user has not provided a specification. We call insert an auxiliary method and insert sort a
primary one in this case.
For the primary method with a partial specification, our analysis proceeds in two steps. Firstly, startingfrom the partial precondition, a forward analysis is conducted to compute the postcondition of the methodin the form of a constraint abstraction [8]. This constraint abstraction is effectively a transfer function for the
method, which may be recursively defined. During this analysis, abductive reasoning may be used wheneverthe current state fails to establish the precondition of the next program command. Secondly, instead of adirect fixpoint computation in the combined abstract domain (with shape, numerical and bag information),a “pure” constraint abstraction (without heap shape information) is derived from the generated constraint
abstraction. This pure constraint abstraction is then solved by fixpoint solvers in pure (numerical and bag)domains, such as [9, 10, 11].
The constraint abstraction of a code segment (e.g. a method) in our settings is an abstract form of
the code segment’s postcondition, given a certain precondition. As the code may contain loops or recursive
calls, its constraint abstraction can also be recursive, or in an open form, accordingly. To illustrate, for thefollowing while loop
while (x>0) { x = x − 1; y = y + 1; }and its precondition {x≥0 ∧ y=0} we have its constraint abstraction as
Q(x, x′ , y, y′ ) ::= x=0 ∧ x=x′ ∧ y=y′ ∨ x>0 ∧ Q(x−1, x′ , y+1, y′ )where we denote x and y as their values before the loop, and the primed versions as the values after theloop execution (we will explain this in more detail in Sec 3). Such constraint abstraction presents thepostcondition of the while loop. Its fixpoint can be achieved with a standard fixpoint calculation process,5with result x≥0 ∧ y=0 ∧ x′ =0 ∧ y′ =x. However, as will be seen later, our constraint abstraction is generally
more complicated involving both shape and pure constraints, requiring us to split them for solution somehow.
As for the example, our forward analysis runs on the body of insert sort to construct the constraint
abstraction. For lines 5-9, it produces a disjunction as the effect of if-else (according to the if-else rule on
Page 19):
Q(x, S, res, T) ::= (post-state of if) ∨ (post-state of else)
where Q represents the post-state of the if-else statement (as well as the method), and its parameters x, S, res
and T are the (program and logical) variables involved in the state.
For the if branch, after the unfolding over llB(x,S) (rule unfold on Page 17), we know from the condition
that the input list x has only one node, and thus its post-state will be∃v · x7→node(v, null) ∧ res=x ∧ S={v}Meanwhile, for the else branch, the list will firstly be unrolled by one node at line 6 (rule unfold), making
x.next point to s (rule assign on Page 19), which references a sub-list one node shorter than the input list
beginning from x:∃S1 , v · x7→node(v, s)∗llB(s,S1 ) ∧ S=S1 ⊔{v}
After that, insert sort is invoked recursively with s. It will consume the precondition (llB(s,S1 )) andensure the postcondition in the form of Q but with corresponding parameters (rule call-inf in Fig. 12). In
that case, the state immediately after symbolic execution of line 7 is∃v, s, S1, r, Sr · x7→node(v, s)∗Q(s, S1, r, Sr ) ∧ |S|>1 ∧ S=S1 ⊔{v}
Note that existential variables (not in the parameter list of Q) are local variables whose quantification may
be omitted for brevity. The state captures the effect of the recursive call (with Q).
Then the forward analysis continues over line 8 to invoke insert. Because the user has provided noannotations for that method, its specifications must be synthesised. For this purpose we replace Q(s, S1 , r, Sr )in second branch with sllB(r,Sr ) ∧ P(s, S1 , r, Sr ) to make explicit the heap portion referred to by r before
we analyse the auxiliary call insert(r, x) (via rule call-unk in Fig. 12). The shape of r comes from thepostcondition of the method, and this is safe because the following entailment relationship is added to ourassumption:
Q(x, S, res, T) ⊢ sllB(res,T) ∧ P(x, S, res, T)
which signifies that Q can be abstracted as a sorted list referenced by res plus some pure constraints P (alsoin constraint abstraction form, whose definition is to be derived in the next step). Our analysis then uses
an augmented technique (details follow slightly later) to synthesise the following specification for insert
based on the symbolic state at the call site:requires sllB(r,S)∗x7→node(v, ) ensures sllB(res,T) ∧ T=S⊔{v}
which indicates that the returned list has the same content as the input list (x) plus {v}. Applying it, we
obtain the following post-state for insert sort:
Q(x, S, res, T) ::= x7→node(v, null) ∧ res=x ∧ S={v} ∨sllB(res,Sres ) ∧ P(s, Ss , r, Sr ) ∧ |S|>1 ∧ S=Ss ⊔{v} ∧ Sres =Sr ⊔{v}
The first disjunctive branch corresponds to the base case, but the second branch now captures the effect of
the recursive call as well as the auxiliary call (to insert). In the base case, the method’s return result (res)refers to one node with value v. The recursive branch signifies that the post-state of the method concerns
the recursive call and the auxiliary call (over s and r), as the constraint abstraction denotes. Note that T
will be not available (as well as its relationship with Sres ) until the next step.
In the second step, we first derive the definition of the pure constraint abstraction P from the above
post-state Q. Each disjunctive branch of Q is used to entail the user-given post-shape (with appropriate
6

instantiations of the parameters). The obtained frames form (via disjunction) the definition of P. For
insert sort, we obtain the following pure constraint abstraction:
P(x, S, res, T) ::= (T=S ∧ |S|=1) ∨ (P(s, Ss , r, Sr ) ∧ |S|>1 ∧ S=Ss ⊔{v} ∧ T=Sr ⊔{v})
We then use pure fixpoint solvers to obtain a closed-form formula |S|≥1 ∧ T=S for P. Based on (2.2), we
now obtain the closed-form approximation for Q:
Q(x, S, res, T) ::= sllB(res,T) ∧ |S|≥1 ∧ T=S
The obtained pure formula is then used to refine the method’s specification as
requires llB(x,S) ∧ |S|≥1 ensures sllB(res,T) ∧ T=S
which imposes more requirements in the precondition, stating that there should be at least one node in thelist to be sorted for the sake of memory safety. With that obligation, the method guarantees that the result
list is sorted and its content remains the same as the input list.
2.2.1. Analysis for the Unannotated Method
The unannotated method insert in the example inserts a node x into a sorted list r. It judges threecases and has a non-tail-recursive call to itself in the last case (to insert x after list r’s head). Since no userannotations are provided for this auxiliary method, our analysis synthesises its (raw) pre- and post-shapes
which are then refined in the same way as for primary methods. The pre-shape is directly synthesised fromthe abstract program state at the call site (x7→node(v,s)∗sllB(r,Sr )). We unroll the recursive call once,
symbolically execute the unrolled method body (starting from the pre-shape) to obtain a post-state, and thenuse the post-state to filter out any invalid post-shapes from the set of possible post-shapes (drawn from allavailable shape predicates). For this example, the possible post-shapes can be (a) sllB(x,S1 )∗sllB(res,S2 ),and (b) sllB(res,S), etc. The symbolic execution gives the following post-state:
x7→node(v, null) ∧ x=res ∨ x7→node(v, r)∗sllB(r,S1 ) ∧ x=res ∧ (∀u∈S1 ·v≤u) ∨r7→node(u, x)∗x7→node(v, null) ∧ r=res ∧ u≤v ∨r7→node(u, x)∗x7→node(v, r1 )∗sllB(r1 ,S1 ) ∧ r=res ∧ u≤v ∧ (∀w∈S1 ·v≤w)
which does not entail the candidate (a), so we filter it out. Taking (b) as the post-shape, we can employ
the same analysis for the primary method to obtain the specification (2.2) (page 6) for insert and continue
with the analysis for the primary method.
2.3. Another Illustrative Example
We illustrate our approach with another more interesting example. We show how the user is expected toprovide shape information for specifications of a primary method, and how our proposed analysis will refinesuch specifications with pure constraints, and derive specifications for loops without annotations.
The method sdl2nbt (Fig 2) converts a doubly-linked sorted list into a node-balanced binary searchtree, as indicated by the shape-only specification in lines 2 and 3. It first finds the “centre” node in the list
(root), where the difference between numbers of nodes to the left and to the right of the centre node is at
most one (lines 5-10), as Fig 3 (a) shows. It then applies the algorithm recursively on both list segments
to the left and to the right of the centre node, and regards the centre node as the tree’s root, whose left
and right children are the resulting subtrees’ roots from the recursive calls (lines 11-17), as in Fig 3 (b) and(c). As the data structures of doubly-linked list and binary tree are homomorphic (line 0), the algorithm
reuses the nodes in the input instead of creating a new tree, making itself in-place. The parameter head inline 1 denotes the first node of the input list, and tail is where the last node’s next field points to. Whenusing this method tail should be set as null initially. The predicates for doubly-linked sorted list segment(sdlB) and node-balanced binary search tree (nbt) are defined in Section 2.1.
7

0 data node2 { int val; node2 prev; node2 next; }1 node2 sdl2nbt(node2 head,9

node2 tail)10}

2 requires sdlB(head, p, q, S)

11

if (head == root) root.prev = null;3 ensures nbt(res, Sres )12

4 { node2 root = head;13

node2 tmp = root.next;

5

node2 end = head;14

if (tmp == tail) root.next = null;

6

while(end != tail) {15

7

end = end.next;168

if (end != tail) {17

end=end.next; root=root.next;}

else root.prev = sdl2nbt(head,root);

else { tmp.prev = null;root.next = sdl2nbt(tmp, tail);}return root;}

Figure 2: The method to convert a sorted doubly-linked list to a node-balanced tree.

t
o
o
r

d
a
e
h
l
l
u
n

1

2

3

d
n
e
4

5

6

l
i
a
t

(a)
t
o
o
r

t
o
o
r
4

4

2
1

6
3

2

5

1

(b)

6
3

5
(c)

Figure 3: Transferring from a sorted doubly-linked list to a node-balanced BST.

To analyse the example, when the forward analysis reaches the while loop at line 6, it discovers that theloop has no user-supplied annotations. In that case, it uses an augmented technique (details follow slightly
later) to synthesise the loop’s pre- and post-shapes, and invoke the analysis procedure recursively to findadditional pure constraints. In this way, we can infer the while loop’s postcondition assdlB(head, null, root, Sh)∗sdlB(root, p, tail, Sr) ∧end=tail ∧ S=Sh ⊔Sr ∧ (∀x∈Sh , y∈Sr ·x≤y) ∧ 0≤|Sr |−|Sh |≤1(1)which indicates that the original list starting from head is cut into two sorted pieces with a cutpoint root.
Meanwhile, the essential constraint (the underlined part, saying the list segment beginning with head is at
most one node shorter than that with root) to ensure the node-balanced property is derived as well.
When the symbolic execution finishes, it generates the following constraint abstraction as the postcondition of the method:8

Q(head, p, q, S, res, Sres ) ::=(†)
root7→node2(v, null, null)∧head=root=res∧tmp=q=tail∧p=null∧S={v}∨ head7→node2(s, null, root)∗root7→node2(v, head, null) ∧ res=root ∧
tmp=q=tail ∧ p=null ∧ S={s, v} ∧ s≤v∨ root7→node2(v, resh , resr )∗Q(head, p, root, Sh, resh , Shres ) ∗Q(tmp, null, tail, Sr, resr , Srres ) ∧ head6=root ∧ root=res ∧ tmp6=tail ∧q=tail ∧ S=Sh ⊔{v}⊔Sr ∧ (∀x∈Sh , y∈Sr ·x≤v≤y) ∧ 0≤|Sr |−|Sh |≤1
where the first two disjunctive branches are base cases of the method’s invocation (where there are only
one and two nodes in the returned tree res, respectively), and the last denotes the effect of recursive calls
combined into the postcondition (where root’s both branches are node-balanced trees). Note that the two
Q’s in the last branch correspond to the invocations of sdl2nbt in lines 12 and 16. Constraints of somelogical variables (like Sres ) will not show up until the next step.
In the second step, to derive the definition of the pure constraint abstraction P from the above post-state
Q, we use each disjunctive branch of Q to entail the user-given post-shape (with appropriate instantiationsof the parameters). During this process, all occurrences of Q are replaced by the post-shape conjoined with
the P according to the entailment relation
Q(head, p, q, S, res, Sres ) ⊢ nbt(res, Sres ) ∧ P(head, p, q, S, res, Sres )The obtained frames (from the Sleek prover [2]) are used to form (via disjunction) the definition of P:
P(head, p, q, S, res, Sres ) ::=(‡)
head=root=res ∧ tmp=q=tail ∧ p=null ∧ S=Sres ={v}∨ head6=root ∧ res=root ∧ tmp=q=tail ∧ p=null∧S=Sres ={s, v} ∧ s≤v∨ P(head, p, root, Sh, resh , Shres ) ∧ P(tmp, null, tail, Sr, resr , Srres ) ∧head6=root ∧ root=res ∧ tmp6=tail ∧ q=tail ∧ S=Sh ⊔{v}⊔Sr ∧Sres =Shres ⊔{v}⊔Srres ∧ (∀x∈Sh , y∈Sr ·x≤v≤y) ∧ 0≤|Sr |−|Sh |≤1
We then use pure fixpoint solvers to obtain a closed-form formula p=null ∧ q=tail ∧ S=Sres ∧ |S|≥1 for P,
and refine the method’s specifications as
requires sdlB(head, p, q, S) ∧ p=null ∧ q=tail ∧ |S|≥1
ensures nbt(res, Sres ) ∧ S=Sres
which proposes more requirements in the precondition, as the head’s prev field should be null, and thewhole list’s last node’s next field must point to tail for termination. Meanwhile, there should be at least
one node in the list for memory safety. With those obligations, the method guarantees that the result is a
node-balanced binary search tree, with the same content as the input list.1
2.3.1. Analysis for the while loop.
The while loop in sdl2nbt (lines 6-10) discovers the centre node of the given list segment referenced byhead. It traverses the list segment with two pointers root and end. The end pointer goes towards the list
segment’s tail twice as fast as root. When end arrives at the tail of the segment (tail), root will point to
the list segment’s centre node.
Instead of requiring users to supply the loop invariant, our analysis regards the loop as a tail-recursive
method and computes its specifications based on the program state in which the loop starts. Our analysis first
synthesises its pre- and post-shapes, and then continues the analysis in the same way as for the main method.
The pre-shape can be abstracted from the program state in which the loop starts. The post-shape synthesis
is done by checking the symbolic execution result of the loop body (unrolled once) against possible abstracted
1 We will explain how to attach the fixpoint result to both pre and post in Sec 4.

9shapes. For this example, we first generate shape candidates according to the variables accessed by the loop,
such as (a) sdlB(head, ph, qh , Sh )∗sdlB(root, pr , qr , Sr ), and (b) sdlB(head, ph, qh , Sh )∗nbt(root, hr, br , Sr ).
Then the unrolled loop body is symbolically executed to filter out those shapes that are not valid to be an
abstraction of postcondition. For this example, executing the loop body yields
head7→node2(v, p, end) ∧ head=root ∧ end=tail ∨head7→node2(vh , p, root)∗root7→node2(vr , head, end) ∧ end=tail(2)

where (b) is directly filtered out since (2) ⊢ (b)∗true fails. However (a) remains a candidate, as (2) ⊢ (a)∗true
holds. Therefore, regarding (a) as a possible post-shape, we can employ the same approach to generate aconstraint abstraction for the while loop, and solve it to obtain formula (1) in page 8.
One more note for the while loop in this example is that the symbolic execution may actually permit morethan one shape to enter as candidates, e.g. sdlB(head,ph , qh , Sh ). Generally this does not affect the analysis
result, as we allow the analysis to continue with all possible postconditions computed from this while loop,
and always choose the most precise final result. In the motivating example, both sdlB(head,ph , qh , Sh ) and(a) are valid shape postconditions for the loop, but later the former one will cause the analysis to fail in line
15/17, because it inappropriately approximates the invariant and hence loses information about root. Since
we synthesise all possible shapes, we can always select those shapes sufficiently strong to support further
analysis to obtain a meaningful result.
3. Language and Abstract Domain
To simplify presentation, we focus on a strongly-typed C-like imperative language in Fig 4. A program
Prog consists of type declarations tdecl, which can define either data type datat (e.g. node) or predicate
spred (e.g. llB), and some method declarations meth. The definitions for spred and mspec are given laterin Fig 5.

Prog
datat
meth
e
d
d[v]

::= tdecl∗ meth∗tdecl ::= datat | spred::= data c { field∗ }field ::= t v
t ::= c | τ::= t mn ((t v)∗ ; (t v)∗ ) mspec∗ {e}τ ::= int | bool | void::= d | d[v] | v=e | e1 ; e2 | t v; e | if (v) e1 else e2 | while (v) {e}::= null | k τ | v | new c(v ∗ ) | mn(u∗ ; v ∗ )::= v.f | v.f :=w | free(v)Figure 4: A Core (C-like) Imperative Language.

The language is expression-oriented, so the body of a method is an expression e, where d (resp. d[v])denotes a heap insensitive (resp. heap sensitive) atom expression. We also allow both call-by-value andcall-by-reference method parameters (which are separated with a semicolon ; where the ones before ; arecall-by-value and the ones after are call-by-reference). We use k τ to denote constants of type τ .
Our specification language (in Fig 5) allows (user-defined) shape predicates to specify both separation andpure properties. The shape predicates spred are constructed with disjunctive constraints Φ. We require thatthe predicates be well-formed [2]. A conjunctive abstract program state, σ, is composed of a heap (shape)
part κ and a pure part π, where π consists of γ and φ as aliasing and numerical (size and bag) information
respectively. We use SH to denote the set of such conjunctive states. During the symbolic execution, theabstract program state at each program point will be a disjunction of σ’s, denoted by ∆. Note that constraint
abstractions (e.g. Q(v∗ )) may occur in ∆ during the analysis. A closed-form ∆ (containing no constraint
abstractions) can be normalised to the Φ form [2]. Pure constraint abstraction P is analogously defined toQ.
10spred
mspec
∆
Φ
Υ
κ
ω
γ
φ
b
s
ϕ
B

::= pred(v∗ ) ≡ Φ::= requires Φpr ensures Φpo∗::= Q(vW ∗) | Φ | ∆1 ∨∆∗2 | ∆∧π | ∆1 ∗∆2 | ∃v·∆::= σ
Wσ ::= ∃v ·κ∧π::= P(v ∗ ) | ω ∗ | Υ1 ∧Υ2 | Υ1 ∨Υ2 | ∃v·Υ::= emp | v7→c(v∗ ) | pred(v∗ ) | κ1 ∗κ2::= ∃v ∗ ·π
π ::= γ∧φ::= v1 =v2 | v=null | v1 6=v2 | v6=null | γ1 ∧γ2::= ϕ | b | a | φ1 ∧φ2 | φ1 ∨φ2 | ¬φ | ∃v · φ | ∀v · φ::= true | false | v | b1 =b2
a ::= s1 =s2 | s1 ≤s2::= k int | v | k int ×s | s1 +s2 | −s | max(s1 ,s2 ) | min(s1 ,s2 ) | |B|::= v∈B | B1 =B2 | B1 ⊏B2 | B1 ⊑B2 | ∀v∈B·φ | ∃v∈B·φ::= B1 ⊔B2 | B1 ⊓B2 | B1 −B2 | {} | {v}

Figure 5: The Specification Language.

The memory model of our specification formulae is adapted from the model given for “early versions” ofseparation logic [6], except that we consider memory cells to be structured records. We assume sets Loc ofmemory locations, Val of primitive values (with 0 ∈ Val denoting null), Var of variables (program and logicalvariables), and ObjVal of object values stored in the heap, with c[f1 7→ν1 , .., fn 7→νn ] denoting an object valueof data type c where ν1 , .., νn are current values of the corresponding fields f1 , .., fn . Let s, h |= ∆ denotethe model relation, with h, s from the following concrete domains:h∈ Heap =df

Loc ⇀fin ObjVals∈ Stack =df

Var → Val ∪Loc

Heaps are finite partial functions mapping locations to values while stacks (stores) are total mappings fromvariables to values or locations, as in the classical separation logic [7, 6]. The detailed model definitions canbe found in Chin et al. [12].
In the analysis we use three kinds of variables in the Var set: program variables, logical variables related
to program variables’ shapes (such as a list’s length), and logical variables to record intermediate states.
For the first two groups we use variables without subscription (such as x and xn), and denote a program
variable’s initial value as unprimed, and its current (and hence final) value as primed [13, 2]. For the thirdgroup, we use subscript ones like x1 and xn1 . For instance, for a code segment x := x + 1; x := x − 2 startingwith state {x>1}, we have the following reasoning procedure:{x′ =x ∧ x>1} x:=x+1 {x>1 ∧ x′ =x+1} x:=x-2 {x>1 ∧ x′ =x1 −2 ∧ x1 =x+1}
where the final value of x is recorded in variable x′ and x1 keeps an intermediate state of x.
4. The Analysis
Our overall analysis algorithm is presented in Fig 6. It takes as input all available specifications andshape predicates, and the code segment to be analysed, together with an optional conjunctive program state
and two variable sequences (mainly for loops and auxiliary methods). The algorithm first recognises the typeof input code segment (mn in line 1). In the first two cases (while loop in line 2 and auxiliary method call inline 3), since we assume no information is given on specifications, some preprocessing work is conducted to
discover possible pre- and post-shapes for the code segment with Preproc (Fig 7). In the case of a primarymethod (line 4), as we assume the shape-based specifications are given by users, no preprocessing is needed.
Our constraint abstraction generation and solving algorithm is then applied to each (partial) specification
11

Algorithm Analysis(T , S, mn, σ, x∗ , y ∗ )1case mn of2| while (w) {e0 } → f := fresh name(); e := if (w) {e0 ; f (x∗ ; y ∗ )};!
(u∗ , v ∗ ) := (x∗ , y ∗ ); ([(Φipr , Φipo )], n) := Preproc(T , S, f, x∗ , y ∗ , e0 , σ, x∗ , y ∗ );!
prim := false;3| t mn ((t u0 )∗ ; (t v0 )∗ ) {e0 } → f := mn; e := e0 ; (u∗ , v ∗ ) := (u∗0 , v0∗ );!
([(Φipr , Φipo )], n) := Preproc(T , S, f, u∗ , v ∗ , e0 , σ, x∗ , y ∗ ); prim := false;
po m
4| t mn ((t u0 )∗ ; (t v0 )∗ ) (requires Φpri ensures Φi )i=1 {e0 } → f := mn;
po n
∗ ∗
∗ ∗
i
i n
!
e := e0 ; (u , v ) := (u0 , v0 ); n := m; (Φpr , Φpo )i=1 := (Φpri , Φi )i=1 ;!
prim := true;5
end case
6
rsps := ∅7
for i := 1 to n do
8
rsp := CA Gen Solve(T , f, e, Φipr , Φipo , u∗ , v ∗ )9
if prim = false and rsp 6= fail then return (f, rsp)
10else if prim = true then rsps := rsps ∪ rsp
11
end if
12 end for
13 return (f, rsps)
end Algorithm
Figure 6: Main analysis algorithm.

Algorithm Preproc(T , S, f, u∗ , v ∗ , e, σ, x∗ , y ∗ )14 sps := [ ];15 prs := SynPre(S, f, u∗ , v ∗ , σ, x∗ , y ∗ )16 for Φpr ∈ prs do
17
pos := SynPost(T , S, f, e, Φpr , u∗ , v ∗ )18
sps := concat(sps, pos)
19 end for
20 return (sps, |sps|)
end Algorithm
Figure 7: Pre-processing algorithm.

to refine it (line 8). Note here we apply a lazy scheme when analysing loops and auxiliary methods: as
the pre-processing may yield a list of possible shape specifications (ordered with heuristics such that the
specifications with higher probability to make the whole verification succeed are more in front), we try eachin sequence. Once a pre/post pair taken from the ordered list (after being refined) leads to the successful
analysis of the enclosing primary method, the other ones in the list are omitted. In this way we try to makeour verification more scalable, as still will be described in later sections.
The pre-processing algorithm mainly invokes the shape synthesis procedures to discover all possible preand post-shapes for loops and auxiliary methods, as shown in lines 15 and 17. Then the list of shape pairs(specifications) are returned and used in further analysis. The details of shape synthesis algorithms will be
introduced in Section 4.3.
4.1. Refining Specifications for Primary Methods
The algorithm for refinement (CA Gen Solve) is given in Fig 8. As illustrated in Section 2.3, the analysis
proceeds in two steps for a primary method with shape information given in specification, namely (1) forward
analysis (at lines 21-22) and (2) pure constraint abstraction generation and solving (at lines 23-30).
12

Algorithm CA Gen Solve(T , mn, e, Φpr ,Φpo ,u∗ ,v ∗ )
21
22
23
24
25
26
27
28

Algorithm Symb Exec
! (T , mn, e, Φpr )∆ := Symb Exec(T , mn, e, Φpr )if ∆ = fail then return fail end if
Wm
Normalise ∆ to DNF, and denote as i=1 ∆iw∗ :={u∗ ,v ∗ ,v ′∗ } ∪ pureV({u∗ ,v ∗ ,v ′∗ }, Φpr ∨Φpo )W∆P := Pure CA Gen(Φpo , Q(w∗ )::= mi=1 ∆i )if ∆P = fail then return fail end if
π := Pure CA Solve(P(w∗ )::=∆P )R := t mn ((t u)∗ ; (t v)∗ ) requires!
ex quan(Φpr , π) ensures ex quan(Φpo , π)
29 if Verify(T , mn, R) then return T ∪ {R} \! { t mn ((t u)∗ ; (t v)∗ ) requires Φpr ensures Φpo }30 else return fail end if

31 errLbls := ∅32 do
33 (∆, l) := |[e]|T mn(Φpr , 0)34 if l>0∧l∈errLbls
/
then
35
Φpr :=ex quan(Φpr ,∆);
36
errLbls := errLbls ∪{l}
37 else if l>0 ∧ l∈errLbls! then return fail
38 end if
39 while l > 0
40 return ∆end Algorithm

end Algorithm
Figure 8: Refining method specifications.

The forward analysis is captured as algorithm Symb Exec to the right of Fig 8. Starting from a given
pre-shape Φpr , it analyses the method body e (via symbolic execution; line 33) to compute the post-state inconstraint abstraction form. The symbolic execution rules are presented in Section 4.4 and they are similar
to symbolic rules used in [2], except for a novel mechanism to derive pure precondition, which we refer toas pure abduction.
This pure abduction mechanism is invoked whenever symbolic execution fails to prove memory safety
based on the current prestate. For example, if we have ll(x, n) as the current state and we require
x7→node( , p) to update the value of p, then it will fail as ll(x, n) does not necessarily guarantee x7→node( , p).
In this case we conduct the pure abduction asll(x, n) ∧ [n≥1] ⊲ x7→node( , p)∗true
to compute the missing pure information (in the square brackets) such that the LHS (including the newly
gained pure part) entails the RHS. The variable errLbls (initialised at line 31) is to record the program
locations in which previous pure abductions occurred. Whenever the symbolic execution fails, it returns astate ∆ that contains the pure abduction result and the location l where failure was detected, as shownin line 33. If the current abduction location l is not recorded in errLbls, it indicates that this is a new
failure. The abduction result is added to the precondition of the current method to obtain a stronger Φpr ,before the algorithm enters the symbolic execution loop with variable errLbls updated to add in the new
failure location l. This loop is repeated until symbolic execution succeeds with no memory error, or aprevious failure point was re-encountered. The latter may indicate a program bug or a specification error,
or may be due to the possible incompleteness of the underlying Sleek prover we use.
For example,
for a method void foo (...) {node w := new node(0, null); goo(w); ...} invoking a method goo(x) withprecondition ll(x, n)∧n≥2, our analysis will perform an abduction to get n≥2 since it is not implied by thecurrent state. However, as n is for the shape of local variable w, it will be quantified away when propagatingn≥2 back, ending up with true being added to foo’s precondition. In the next round of symbolic execution,
our analysis will have the same abduction at the same point.
Back to the main algorithm CA Gen Solve, the analysis next builds a heap-based constraint abstraction,
named Q(w∗ ), for the post-state in line 23. This constraint abstraction is possibly recursive. (Definition †on page 8 is an example of this heap-based abstraction.) We then make use of another algorithm in Fig 9,
named Pure CA Gen, to extract a pure constraint abstraction, named P(w∗ ), without any heap property.
(Definition ‡ on page 9 is an instance of this pure abstraction.) This algorithm tries to derive a branch Pi
13

for each branch ∆i of Q. For every ∆i it proceeds in two steps. In the first step (lines 42-44), it replaces therecursive occurrence of Q in ∆i with σ∗P(w∗ ). In the second step (lines 45-46) it tries to derive Pi via theentailment. If the entailment fails, then pure abduction is used to discover any missing pure constraint σi′for ρ∆i to allow the entailment to succeed. In this case, σi′ is incorporated into σi (and eventually Pi ). Once
this is done, we use some existing fixpoint analysis (e.g. [10]) inside Pure CA Solve to derive non-recursive
constraint π, as a simplification of P(w∗ ). This result is then incorporated into the pre/post specifications inline 28, before we perform a post verification in line 29 using the Hip verifier [2], to ensure the strengthened
precondition is strong enough for memory safety.
Two auxiliary functions used in the algorithm are described here. The function pureV(V, ∆) retrieves
from ∆ the shapes referred to by all pointer variables from V , and returns the set of logical variables
used to record numerical (size and bag) properties in these shapes, e.g. pureV({x}, ll(x, n)) returns {n}.
This function is used in the algorithm to ensure that all free variables in Φpr and Φpo are added into theparameter list of the constraint abstraction Q. The function ex quan(∆, π) is to strengthen the state ∆ withthe abduction result π: ex quan(∆, π) =df ∆ ∧ ∃(fv(π) \ fv(∆)) · π. It is used to incorporate the discovered
missing pure constraints into the original specification. For example, ex quan(ll(x, n), 0<m ∧ m≤n) returnsll(x, n) ∧ 0<n.
Algorithm Pure CA Gen(σ, Q(w∗ )::=

Wm

i=1 ∆i )41 for i = 1 to m
42 Denote all appearances of Q(w∗ ) in ∆i as Qj (wj∗ ), j = 1, ..., p
43 Denote substitutions ρj = [([wj∗ /w∗ ]σ∗P(wj∗ ))/Qj (wj∗ )]44 Let substitution ρ := ρ1 ◦ ρ2 ◦ ... ◦ ρp as applying all substitutions!
defined above in sequence
45 if (ρ∆i ⊢ σ∗σi or ρ∆i ∧ [σi′ ] ⊲ σ∗σi ) and ispure(σi ) then Pi := σi
46 else return fail end if
47 end forW
48 return m
i=1 Piend Algorithm
Figure 9: Pure constraint abstraction generation algorithm.

4.2. Pure abduction mechanism
We use the Sleek prover [2] to check ∆1 entails ∆2 . If the entailment holds it also derives ∆3 (a.k.a.
frame) such that ∆1 ⊢ ∆2 ∗∆3 . However, if it fails, we assume that the shape information is sufficiently
provided, and use our pure abduction mechanism (σ1 ∧ [σ ′ ] ⊲ σ2 ∗σ3 in Fig 10) to discover missing pureconstraints σ ′ so that σ1 ∧ σ ′ ⊢ σ2 ∗σ3 .
Our pure abduction deals with three different cases. The first rule (R1) applies when the LHS (σ) does
not entail the RHS (σ1 ) but the RHS entails the LHS with some pure formula (σ ′ ) as the frame; e.g. inll(x, n) 0 x7→node( , null), the RHS can entail the LHS with pure frame n=1. The abduction then checks
to ensurell(x, n) ∧ n=1 ⊢ x7→node( , null)∗σ2 for some σ2 , and returns the result n=1. Note the check
ispure(σ ′ ) ensures that σ ′ contains no heap information.
In the second rule (R2), neither side entails the other but the LHS term could be unfolded. An example
is σ = sllB(x, S), σ1 = x7→node(u, p)∗p7→node(v, null). As the shape predicates in the antecedent areformed by disjunctions according to their definitions (like the sllB), certain branches of σ may entail σ1 . As
the rule suggests, to accomplish abduction σ ∧ [σ ′ ] ⊲ σ1 ∗σ2 , we first unfold σ and try entailment or further
abduction with the results (σ0 ) against σ1 . If it succeeds with a pure frame σ ′ , then we confirm the abduction
by checking σ ∧ σ ′ ⊢ σ1 ∗σ2 . For the example above, the abduction returns |S|=2 (σ ′ ) and discovers thenontrivial frame S={u, v}∧u≤v (σ2 ). Note that function data no returns the number of data nodes in a state,14

σ 0 σ1 ∗true σ1 ⊢ σ∗σ ′ispure(σ ′ )σ ∧ σ ′ ⊢ σ1 ∗σ2σ ∧ [σ ′ ] ⊲ σ1 ∗σ2(R1)σ 0 σ1 ∗true σ1 0 σ∗true σ0 ∈ unroll(σ) data no(σ0 ) ≤ data no(σ1 )(σ0 ⊢ σ1 ∗σ ′ or σ0 ∧ [σ0′ ] ⊲ σ1 ∗σ ′ ) ispure(σ ′ ) σ ∧ σ ′ ⊢ σ1 ∗σ2σ ∧ [σ ′ ] ⊲ σ1 ∗σ2σ 0 σ1 ∗true σ1 0 σ∗true σ1 ∧ [σ1′ ] ⊲ σ∗σ ′ispure(σ ′ ) σ ∧ σ ′ ⊢ σ1 ∗σ2σ ∧ [σ ′ ] ⊲ σ1 ∗σ2

(R2)

(R3)

Figure 10: Pure abduction rules.

e.g. it returns one for x7→node(v, p)∗ll(p, m). (This syntactic check is important for the termination of theabduction.)
Wu The unroll operation unfolds all shape predicates once in σ, normalises the result to a disjunctive
form ( i=1 σ i ), and returns the result as a set of formulae ({σ 1 , ..., σ u }). An instance is that it expands
x7→node(v, p)∗ll(p, m) to be {x7→node(v, p) ∧ p=null ∧ m=0, ∃u, q, k · x7→node(v, p)∗p7→node(u, q)∗ll(q, q) ∧m=k+1}.
In the third rule (R3), neither side entails the other and the LHS term cannot be unfolded. This happens
often during the abstraction stage in the analysis when we need to fold up a “concrete” state of nodes against
an abstracted shape predicate, e.g., when σ = x7→node(u, p)∗p7→node(v, null) and σ1 = ∃S · sllB(x, S). In
this case, the rule swaps the two sides of the entailment and applies the second rule (R2) to uncover thepure constraints σ1′ and σ ′ . It checks that adding σ ′ to the LHS (σ) entails the RHS (σ1 ) before it returns
σ ′ . For the example, the abduction returns u≤v which is essential for the two nodes to form a sorted list
(RHS). Note that the rule (R3) is only allowed to be applied once in one abduction query to avoid infinite
number of swapping (between (R2) and (R3)).
Example 1. For example, to verify the append procedure used in quick sort, the given precondition signifies
the two inputs are sorted lists, sll(x, xn, xs, xl)∗sll(y, yn, ys, yl), and the postcondition is sll(x, m, rs, rl).
By using our abduction mechanism, our analysis can find out that xl ≤ ys which indicates that the largest
element in the first list should be less than or equal to the smallest element in the second list which makes
the functionality of append correct.
4.3. Inferring Specifications for Auxiliary Methods and Loops
For auxiliary methods2 , we conduct a pre-analysis (Fig 11) to synthesise the pre- and post-shapes before
we conduct the refinement analysis from Fig 8. Loops are dealt with by analysing their tail-recursive versions
in the same way. This approach alleviates the need for users to provide specification annotations for bothloops and auxiliary methods.
The pre-shape synthesis algorithm SynPre (Fig 11 left) takes in as input the set of shape predicates(S), the auxiliary method name (f ), its formal parameters (u∗ , v ∗ ), the current symbolic state in which
f is called (σ), and the corresponding actual parameters (x∗ , y ∗ ) of the invocation. The algorithm firstobtains possible shape candidates from the parameters u∗ , v ∗ with ShpCand (line 49), then picks up a soundabstraction for the method’s pre-shape with entailment, and filters out the ones which fail (line 52). Finallythe pre-shape abstraction is returned. While we use an enumeration strategy here, the number of possible
shape candidates per type is small as it is strictly limited by what the user provides in the primary methods,
and then filtered and prioritised by our system.
2 In practice, we treat methods without user-specified shape specifications as auxiliary.

15

Algorithm SynPre∗ ∗∗ ∗! (S, f, u , v , σ, x , y )
49
50
51
52
53
54

C := ShpCand(S, u∗ , v ∗ )for σC ∈ C do
if σ 0 [x∗ /u∗ , y ∗ /v ∗ ]σCthen C:=C\{σC } end if
end forreturn C

end Algorithm

Algorithm SynPost (T , S, f, e, Φpr , u∗ , v ∗ )
55
56
57
58
59
60
61

C := ShpCand(S, u∗ , v ∗ )T ′ :=T ∪{f (u∗ ,v ∗ ) requires Φpr ensures false {e}}∆ := Symb Exec(T ′ , f, syn unroll(f, e), Φpr )for σC ∈ C do
if ∆∧[σ] ⋫ σC then C := C\{σC } end if
end forreturn pair spec list(Φpr , C)

end Algorithm
Figure 11: Shape synthesis algorithms.

To synthesise post-shapes (SynPost, Fig 11 right), we also assign C as possible shape candidates (line55). We unroll f ’s body e once (i.e. replace recursive calls to f in e with a substituted e) and symbolically
execute it (line 57), assuming f has a specification requires Φpr ensures false (line 56). The postcondition
false is used to ensure that the execution only considers the effect of the program branches with no recursive
calls (to f itself).We then use ∆ to find out appropriate abstraction of post-shape (line 59),which is pairedwith Φpr and returned as result. Here we use pure abduction to filter post-shapes to preserve as many
shapes that are potentially refinable as possible. The function pair spec list(Φpr , C) forms an ordered list ofpre-/post-shape pairs, each of which has Φpr as pre-shape and a Φpo in C as post-shape.
We illustrate our procedure to generate and confirm candidate shape abstractions (ShpCand) with an
example. If we have two parameters x and y with type node, and the user has defined two shape predicatesllB and sllB with node, then the list of all possible shape candidates for the two variables (C) will be[sllB(x, S)∗sllB(y, T), llB(x, S)∗sllB(y, T), sllB(x, S)∗llB(y, T), llB(x, S)∗llB(y, T), sllB(x, S), sllB(y, S),llB(x, S), llB(y, S), emp]. Elements of this list will be checked against appropriate abstract states (line 5152 in Fig 11 left and line 59 in Fig 11 right) where unsound elements will be eliminated. For example, inthe previous list, only llB(x, S)∗llB(y, T) remains in the list and participates in further verification, given
σ = x7→node(u, p)∗p7→node(v, null)∗y7→node(s, q)∗q7→node(t, null).
The initial experimental results confirm that our shape synthesis keeps only highly relevant abstractions.
For the while loop in Section 2.3, we filtered out 24 (of 26) abstractions. Generally, in case that there areseveral abstractions as candidate specifications, we employ some other mechanisms to reduce them further.
Firstly, we prioritise post-shapes with same (or stronger) predicates as in precondition since it is more likelythat the output will have the same or similar shape predicates as the input, e.g. x is expected to remain
as sllB (or stronger) if it points to sllB as input. Secondly, we employ a lazy scheme when refining thesynthesised pre/post-shapes (to complete specifications). We retrieve (and remove) the pre/post-shape pairfrom the head of the list, (1) use the refinement algorithm (Fig 8) to obtain a specification for the auxiliary
method, and (2) continue the analysis for the primary method. If the analysis for the primary method
succeeds, we will ignore all other synthesised pre/post-shapes from the list. If either (1) or (2) fails, wewill try the next one from the list. Note that our synthesis of shape specification could only cater to one
predicate per parameter/result. In cases where more complex shape specifications are needed, we allow users
to specify them directly for the respective auxiliary method. These mechanisms help to keep attempts overcandidate specifications at a minimum level.
4.4. Symbolic Execution Rules
This section defines the symbolic execution rules used in the first step of the constraint abstraction
generation. If the program contains recursive calls to itself, the postcondition will be in a recursive (open)form.
The type of our symbolic execution is defined as16

|[e]| =df AllSpec → Names → (PSH × Int) → (PSH × Int)
where |[e]| takes as its first parameter the set of method specifications and as its second parameter the nameof the current method. The integer (label) in both input and output is used to record a program location
where abduction is needed. If the label remains zero after the symbolic execution of e, then the output state
denotes the post-state of e. A positive label indicates that an abduction has occurred and the resulting state(the abduction result) will be propagated back to the method’s precondition by our analysis, and the next
round of symbolic execution will be required.
The foundation of the symbolic execution is the basic transition functions from a conjunctive abstractstate to a conjunctive or disjunctive abstract state below:
unfold(x) =df SH → PSH[x]Unfoldingexec(d[x]) =df (AllSpec×Names) → (SH[x]×Int) → (SH×Int) Heap-sensitive exec.
exec(d)=df (AllSpec×Names) → (SH×Int) → (SH×Int)

Heap-insensitive exec.

where SH[x] denotes the set of conjunctive abstract states in which each element has x exposed as the head ofa data node (x7→c(v∗ )), and PSH[x] contains all the (disjunctive) abstract states, each of which is composedby such conjunctive states. unfold(x) unfolds the symbolic heap so that the cell referred to by x is exposed
for access by heap sensitive commands d[x] via the second transition function exec(d[x]). The third function
exec(d) defined for other (heap insensitive) commands d does not require such exposure of x.
For the unfolding operation unfold(x), there are two possible scenarios. If x refers to a data node in thecurrent state σ, no unfolding is required and the exec operation can proceed directly. However, if x refers toa (user-defined) shape predicate, then unfold(x) will unfold the current state σ according to the definitionof the predicate in order to expose the data node referred to by x:
unfold(x)(x7→c(v∗ )∗σ)x7→c(v∗ )∗σc(root, v ∗ )≡Φ
unfold(x)(c(x, u∗ )∗σ)σ∗[x/root, u∗ /v ∗ ]ΦThe symbolic execution of heap-sensitive commands d[x] (i.e. x.f, x.f := w, or free(x)) assumes thatthe unfolding unfold(x) has been done prior to the execution. The first three rules below are for normal
symbolic execution where the current state is sufficiently strong for safe execution. The last two rules handle
the cases where the symbolic execution fails and abductive reasoning can be used to discover missing pure
information.
σ ⊢ x7→c(v1 , .., vn )∗σ ′exec(x.fi )(T ,f )(σ, 0)(σ ′ ∗c(x, v1 , .., vn ) ∧ res=vi , 0)σ ⊢ x7→c(v1 , .., vn )∗σ ′exec(x.fi := w)(T ,f )(σ, 0)(σ ′ ∗c(x, v1 , .., vi−1 , w, vi+1 , .., vn ), 0)σ ⊢ x7→c(u∗ )∗σ ′exec(free(x))(T ,f )(σ, 0)(σ ′ , 0)σ 0 x7→c(u∗ )∗true σ∗[σ ′ ] ⊲ x7→c(u∗ )∗true
exec(d[x])(T ,f )(σ, 0)(σ ′ , lbl(d[x]))σ 0 x7→c(u∗ )∗true σ∗[σ ′ ] ⋫ x7→c(u∗ )∗true
exec(d[x])(T ,f )(σ, 0)

17(false, lbl(d[x]))Note that the second to last rule uses an abductive reasoning (via Sleek) to discover the missing numericalinformation σ ′ . Here we use a mapping lbl(−) to map any instruction in the program being analysed to aunique positive integer label (namely the aforementioned program location). The rule changes the second
element of the result to lbl(d[x]) which will be used by the analysis to record the instruction causing an
abduction, quits the current execution, propagates the discovered information back to the precondition of thecurrent method, and restarts the symbolic execution with the strengthened precondition. The last rule covers
the scenario in which the abduction fails.Then the execution cannot continue and returns (false, lbl(d[x])).

exec(k)(T ,f )(σ, 0)(σ ∧ res=k, 0)

exec(v)(T ,f )(σ, 0)exec(new c(v ∗ ))(T ,f )(σ, 0)(x∗ , y ∗ ) = vars(w, e)(σ ∧ res=v, 0)(σ∗res7→c(v∗ ), 0)(g, T1 ) = Analysis(T , while(w){e}, σ, x∗ , y ∗ ) T ′ = T ∪T1

exec(while(w){e})(T ,f )(σ, 0)nt mn ((ti ui )mi=1 ; (ti vi )i=1 ) ∈ T

WHILE

exec(g(x∗ ; y ∗ ))(T ′ , f )(σ, 0)(mn, T1 ) = Analysis(T , mn, σ, x∗ , y ∗ ) T ′ = T ∪T1

exec(mn(x1 ..xm ; y1 ..yn ))(T ,f )(σ, 0)exec(mn(x1 ..xm ; y1 ..yn ))(T ′ ,f )(σ, 0)nt mn ((ti ui )mmn6=f
i=1 ; (ti vi )i=1 ) requires Φpr ensures Φpo ∈ T′′ m′ρ = [xi /ui ]i=1 ◦ [yi /vi′ ]ni=1 σ ⊢ ρΦpr ∗σ ′ ρo = [yi /vi ]ni=1 ◦ ρρl = [ri /yi′ ]ni=1
ρol = [ri /yi ]ni=1
fresh logical ri((ρl σ ′ )∗(ρol ◦ ρo Φpo ), 0)exec(mn(x1 ..xm ; y1 ..yn ))(T ,f )(σ, 0)

CALL-VERnt mn ((ti ui )m
mn=f
i=1 ; (ti vi )i=1 ) requires Φpr ensures Φpo ∈ T
′
′ n
′
n
ρ = [x′i /u′i ]m
◦
[y
/v
]
σ
⊢
ρΦ
∗σ
ρ
=
[y
/v
]
pr
o
i i i=1 ◦ ρi=1i i i=1
ρl = [ri /yi′ ]ni=1
ρol = [ri /yi ]ni=1
fresh logical riexec(mn(x1 ..xm ; y1 ..yn ))(T ,f )(σ, 0)((ρl σ ′ )∗(ρol ◦ ρo (Φpo ∧P(u∗ , v ∗ ))), 0)′′ n
ρ = [x′i /u′i ]mi=1 ◦ [yi /vi ]i=1

σ 0 ρΦpr ∗true σ ∧ [σ ′ ] ⊲ ρΦpr ∗true

t mn...∈T

exec(mn(x1 ..xm ; y1 ..yn ))(T ,f )(σ, 0)t mn...∈T′′ n
ρ = [x′i /u′i ]mi=1 ◦ [yi /vi ]i=1

(σ ′ , lbl(mn(...)))σ 0 ρΦpr ∗true σ ∧ [σ ′ ] ⋫ ρΦpr ∗true

exec(mn(x1 ..xm ; y1 ..yn ))(T ,f )(σ, 0)(false, lbl(mn(...)))

CALL-UNK

CALL-INF

CALL-ABD

CALL-FAIL

Figure 12: Symbolic execution rules for heap-insensitive commands.

The symbolic execution rules for heap-insensitive commands are listed in Fig. 12. The first three rules deal
with constant (k), variable (v) and data node creation (new c(v ∗ )), respectively, while the remaining rules
handle method invocation. The fourth rule (WHILE) and fifth rule (CALL-UNK) are used for the invocationof a while loop or an auxiliary method which has not been analysed, where we employ the analysis algorithm
recursively to achieve its postcondition to enable application of the next rule. The sixth rule (CALL-VER)
is used for the invocation of another method mn which has already been analysed (mn6=f ), and the callsite meets the precondition of mn, as checked by the entailment σ ⊢ ρΦpr ∗σ ′ . In this case, the execution18

succeeds and moves on. The seventh rule (CALL-INF) is for a recursive call to the current method (mn=f ),similar as above except that a constraint abstraction is in place as postcondition. The last two rules arefor the cases where abductive reasoning is employed (CALL-ABD) and where the call site cannot establish
the precondition of the callee method (CALL-FAIL). In both cases, the execution discontinues. The eighth
rule returns the abduction result σ ′ , which is a pure formula and will be propagated back by the analysis
to strengthen the caller method’s precondition. The last rule captures the scenario in which the abduction
fails. Note that the operator ◦ is used to compose two substitutions: the substitution ρ2 ◦ρ1 works by first
applying ρ1 and then ρ2 .
To keep presentation simple, we assume there are no mutual recursions in the programs to analyse;
therefore each method to be analysed should only call itself recursively. This assumption does not lose
generality, as we can always transform mutual recursion into single recursion [14] to have only one constraint
abstraction Q in our analysis for one method.
The following rule for all commands signifies that when starting from a configuration in which the second
element is positive (i.e. a faulty state), the execution will not change the state. This rule is used to skip
all remaining instructions when abductive reasoning is used as a new round of symbolic execution withstrengthened precondition should be started instead:l>0
exec(−)(T ,f )(σ, l)(σ, l)

We can now lift unfold’s domain to PSH using the following operation unfold† :__unfold† (x) σi =df(unfold(x)σi )and similarly for exec:
W
exec† (d)(T ,f )( σi , l) =df

W( σi′ , max{li }) where (σi′ , li ) ∈ exec(d)(T ,f )(σi , l)The symbolic execution rules for program constructors e can now be defined using the lifted transition
functions above. Firstly, no change will be made if starting from a faulty state, as the first rule shows. In allother cases, the symbolic execution transforms one abstract state to another w.r.t. the program instruction:|[−]|T f (∆, l)=df (∆, l), where l > 0|[d[x]]|T f (∆, 0) =df exec† (d[x])(T ,f )(unfold† (x)∆, 0)|[d]|T f (∆, 0)=df exec† (d)(T ,f )(∆, 0)|[e1 ; e2 ]|T f (∆, 0) =df |[e2 ]|T f ◦ |[e1 ]|T f (∆, 0)|[v := e]|T f (∆, 0) =df [v1 /v ′ , r1 /res](|[e]|T f (∆, 0)) ∧ v ′ =r1 , fresh v1 , r1(∆′1 , l1 ) = |[e1 ]|T f (v∧∆, 0)(∆′2 , l2 ) = |[e2 ]|T f (¬v∧∆, 0)|[if (v) e1 else e2 ]|T f (∆, 0) =df (∆′1 ∨ ∆′2 , max{l1 , l2 })
4.5. Soundness and Termination
In this section we discuss about the soundness of our analysis and show that our analysis is also terminating.
Before proceeding to the soundness property, recalling that we have both unprimed variables (for theirinitial values in abstract states) and primed ones (for their current values), we realise that the concrete
program states should always be linked to the primed ones. For this reason we have the following definition:
Definition 1 (Poststate). Given an abstract state ∆, Post(∆) captures the relation between primed variablesof ∆. That is,Post(∆) =df ρ(∃V · ∆), whereV = {v1 , . . . , vn } denotes all unprimed program variables in ∆, andρ = [v1 /v1′ , . . . , vn /vn′ ].
19For example, for ∆ = Node(x′ , v′ , y′ ) ∧ v′ =v ∧ y′ =null, we have Post(∆) = Node(x, v, y) ∧ y=null.
The soundness of our analysis is defined as follows:
Definition 2 (Soundness). For a method definition t mn ((t u)∗ ; (t v)∗ ) {e}, if our analysis refines its
specification as t mn ((t u)∗ ; (t v)∗ ) requires Φpr ensures Φpo {e}, then for all s, h |= Φpr , the execution fromhs, h, ei never gets stuck; and if hs, h, ei֒→∗ hs′ , h′ , νi for some value ν, then we have s′ , h′ |= Post(Φpo ).
The underlying operational semantics of our language was given in Chin et al. [12], where the small-steptransition relation is of the form hs, h, ei֒→hs′ , h′ , e′ i. Its concrete program state consists of stack s and heaph, as described in Section 3. Chin et al. [12] also defines the relation s, h |= ∆ and the (transitive closure)
relation hs, h, ei֒→∗ hs′ , h′ , νi which terminates with a value ν in some finite number of steps.
In our analysis, the synthesised missing specifications are discovered with the help of abduction andfixpoint calculators (to ensure convergence). The fixpoint calculators call join and widening operators
over the numerical and bag domains. The join and widening operations usually weaken the pre-/postconditions. Weakening a postcondition is deductively sound. However, weakening a precondition may cause
the synthesised precondition unsafe for the method being analysed.
Meanwhile, if the given predicates used in pre-/post-shape templates are not good enough to describe
the obligation of memory safety, our refinement of the precondition might not be sufficient for the program
to execute safely without inappropriate memory access. For example, if our analysis is only supplied with alist shape predicate without any other information (such as length or content), then our analysis can neverobtain a memory safety requirement like “the length of the input list should be at least n”, even if it isneeded for memory safety of the method.
So after the specification refinement, we apply the verification system Hip/Sleek [12] to verify the
program against the refined specifications so as to rule out any incorrect specifications (obtained due to theabove-mentioned reasons), as shown in line 29 of our refinement algorithm in Figure 8. The soundness of
our analysis is established by the soundness of the verification system Hip/Sleek (given in [12]).
Theorem 1 (Termination). Our analysis terminates in a finite number of steps for a program with a finite
number of partial specifications and a finite set of user-defined predicates.
From the main analysis algorithm, we can see that the termination of our analysis relies on two points:
the termination of fixpoint solver for any numerical and bag constraint abstraction and the termination of
abduction. The termination of fixpoint solver has been proved [10, 11]. The non-termination problem of
abduction may be caused by infinite number of unrolling in rule (R2), or infinitely recursive application ofrule (R3). To prevent the problem, we have two restrictions when we apply the abduction rules: (i) thedata no check in (R2) which ensures that the unroll operation is not applied infinitely; (ii) the third rule (R3)
is not allowed to be applied twice in one abduction query, which prevents the infinite swapping problem.
5. Experiments and Evaluation
We have implemented a prototype system for evaluation. Our experimental results were achieved with anIntel Core 2 CPU 2.66GHz with 8Gb RAM. The four columns in the tables (Fig. 13 and Fig. 14) describe,
respectively, the analysed programs, the analysis time in seconds, and the primary methods’ (given andinferred) preconditions and postconditions. All formulae with a grey background are inferred by our analysis.
For some programs, we have verified them with different pre/post shape templates. Programs with star ∗have different versions for various data structures. The shape predicates used in the experiment but notpreviously given in paper are defined in Appendix A.
The results highlight the refinement of both pre- and postconditions based on user-provided shape specifications, even for complicated data structures such as AVL and red-black trees. Firstly, our approach
can compute non-trivial pure constraints for postconditions, e.g. for create we obtain the value range inthe created list, for delete we know the content of the result list is subsumed by that of the input list,
20

Prog.
TimePre
List processing programs
0.379
emp ∧ n≥0create∗sort
insert∗tailinsertrand
insert∗deletePostllB(res, S) ∧ n=|S| ∧ ∀v∈S·1≤v≤n

1.752

emp ∧ n≥0dllB(res, rp, S) ∧ n=|S| ∧ ∀v∈S·1≤v≤n

0.954

emp ∧ n≥0

sllB2(res, S) ∧ n=|S| ∧ ∀v∈S·1≤v≤n

0.591
0.789

ll(x, n) ∧ n≥1
dll(x, p, n) ∧ n≥1ll(x, m) ∧ m=n+1
dll(x, q, m) ∧ n≥1 ∧ m=n+1 ∧ p=q

0.504

sll(x, n, xs, xl)∧ v≥xs

sll(x, m, mn, mx)∧ xs=mn∧mx=max(xl,v)∧m=n+1

0.566
0.628
0.522
0.830

ll(x, n) ∧ n≥1
sll(x, n, xs, xl)∧ v≥xlll(x, n) ∧ n≥1
dll(x, p, n) ∧ n≥1ll(x, m) ∧ m=n+1
sll(x, m, mn, mx) ∧ v=mx ∧ mn=xs ∧ m=n+1
ll(x, m) ∧ m=n+1
dll(x, q, m) ∧ m=n+1 ∧ p=q—

sll(x, n, xs, xl)∧ (fail)sll(x, m, mn, mx)∧ (fail)

0.630

llB(x, S) ∧ |S|≥2

llB(x, T) ∧ ∃a.S=T⊔{a}

1.024

sllB(x, S) ∧ |S|≥2

sllB(x, T) ∧ ∃a.S=T⊔{a}

0.296ll(x, m)∧ n≥0∧m≥nls(x, p,k)∗ll(res, r)∧ p=res∧k=n∧m=n+r

2.205

sllB(x, S) ∧ n≥0∧|S|≥n0.512ll(x, xn)∗ll(y, yn)∧ xn≥1dll(x, xp, xn) ∗dll(y, yp, yn) ∧ xn≥1sll(x, xn, xs, xl)∧ xl≤ys∗sll(y, yn, ys, yl)

travrsappend∗

0.660
0.948

slsB(x, p, T)∗sllB(res, S2 )∧ p=res∧|T|=n∧ S=T⊔S2 ∧ ∀u∈T,v∈S2 · u≤vll(x, m) ∧ m=xn+yn
dll(x, q, m) ∧ m=xn+yn ∧ q=xp
sll(x, m, rs, rl) ∧ yl=rl ∧ m≥1+yn ∧ m=xn+yn

Figure 13: Experimental Results.

for list-sorting algorithms we confirm the content of the output is the same as that of the input, and fortree-processing programs (insert, delete and avl ins), we obtain that the height difference between the
input and output trees is at most one. Meanwhile, we can calculate non-trivial requirements in precondition
for memory safety or functional correctness. As an example, the travrs method, taking in a list with lengthm and an integer n, traverses towards the tail of the list for n steps. The analysis discovers m≥n in theprecondition to ensure memory safety. Another example is the append method concatenating two sorted
lists into one. To ensure that the result list is sorted, the analysis figures out that the minimum value in thesecond list must be no less than the maximum value in the first list.
A second highlight is our flexibility by supporting multiple predicates. Our analysis tries to refine
different specifications for the same program at various correctness levels (with different predicates), e.g.
sort insert and append. For rand insert, which inserts a node into a random place (after the head) of alist, we confirm that the list’s length is increased by one, but cannot verify the list is kept sorted if it was
before the insertion, as the result indicates.
Another highlight is that we can reduce user annotations by synthesising specifications for auxiliary methods, given raw specifications of primary methods. For example, we have analysed a number of list-sorting
algorithms with at least one auxiliary method each. We list two auxiliary methods (merge for merge sortand flatten for tree sort) and their discovered specifications. Note that these sorting algorithms havethe same specification for their primary methods (line ∗). Further examples, avl ins and rbt ins also havesome auxiliary (recursive) methods such as calculation of tree’s height, which are automatically analysed21

Prog.
Time
Sorting programs
Sorting (main)

Pre

Post

llB(x, S) ∧ |S|≥1

sllB(res, T) ∧ T=S

(∗)

merge

4.107

sllB(x, Sx )∗sllB(y, Sy )sllB(res, T) ∧ T=Sx ⊔Syflatten2.693

bstB(x, S)

sllB(res, T) ∧ T=S

insert0.824

sllB(r, S)∗x7→node(v, )sllB(res, T) ∧ T=S⊔{v}

quick

2.132

llB(x, S)heightinsert

0.913
1.276

bt(x, S, h)bt(x, S, h) ∧ |S|≥1 ∧ h≥1bt(x, T, k) ∧ res=h=k ∧ S=T
bt(x, T, k) ∧ T=S⊔{v} ∧ h≤k≤h+1

delete0.970

bt(x, S, h) ∧ |S|≥2 ∧ h≥2bt(x, T, k) ∧ ∃a.S=T⊔{a} ∧ h−1≤k≤hsearch1.583

bst(x, sm, lg)bst(x, mn, mx) ∧ sm=mn ∧ lg=mx ∧ 0≤res≤1

bst
insert1.720

bst(x, sm, lg)

avl ins

11.12

avl(x, S, h)avl(res, T, k) ∧ T=S⊔{v} ∧ h≤k≤h+1

rbt ins

8.76

rbt(x, S, 0, h)

rbt(res, T, 0, k) ∧ T=S⊔{v} ∧ h≤k≤h+1

sdl2nbt

5.826

sdlB(x, p,q,S)∧ |S|≥1∧
p=null ∧ q=tailnbt(res, T) ∧ T=S

llB(x, S1 )∗llB(res, S2 ) ∧ S=S1 ⊔S2 ∧∀u∈S1 , v∈S2 · u≤p≤v
Binary tree, binary search tree, AVL tree and red-black tree processing programs
travrs0.532
bt(x, S, h)bt(x, T, k) ∧ S=T ∧ h=k
count
0.709
bt(x, S, h)bt(x, T, k) ∧ res=|S| ∧ S=T ∧ h=k

bst(x, mn, mx) ∧ (v<sm∧v=mn∧lg=mx∨
lg<v∧v=mx∧sm=mn ∨ sm=mn∧lg=mx)

Figure 14: Experimental Results. (Cont.)

as well. To have better efficiency, we advocate the use of smaller predicates to capture different aspects ofcomplex data structures separately. As an example, the predicate rbt used for analysing rbt ins capturescontents and red-black colours only, leaving the binary search property to a separate predicate, e.g. bstB.
We have also tried our approach over part of the FreeRTOS kernel [15]. For its list processing programs
list.h and list.c (472 lines with intensive manipulation over composite sorted doubly-linked lists) it took
2.85 seconds for our prototype to refine all the specifications given for the main functions, which further
confirms the viability of our approach.
6. Related Work and Conclusion
6.1. Related works
In recent years, dramatic advances have been made in automated verification of pointer safety for heapmanipulating programs. We highlight some of them here. The local shape analysis by Distefano et al. [4]was able to infer automatically loop invariants for list-processing programs, which formed the early-version
SpaceInvader tool. Gotsman et al. [16] proposed an interprocedural shape analysis for the SLAyer tool.
Berdine et al. [17] extended the local shape analysis [4] to handle higher-order list predicate so that more
complicated real-world data structures can be analysed. Yang et al. [5] proposed a novel abstraction operation which significantly improves the scalability of the analysis. Recently, more large industrial code canbe verified by the SpaceInvader/Abductor tool using the compositional analysis with bi-abductive inference [3, 18]. Due to their focus on a single shape domain, only heap information can be dealt with in their22

bi-abduction. However, in real code, additional information (e.g. numerical properties) may be needed evenjust for the verification of memory safety (e.g. red-black trees widely used in Linux Kernel). Compared with
their work, our analysis focuses on a combined abstract domain in the presence of user-defined predicates,
covering shape, numerical and bag information. Our analysis can deal with examples that cannot be handled by their work, as shown in the previous section, e.g. the travrs example for memory safety, the sorting
examples and the avl tree, red-black tree examples for memory safety as well as functional correctness.
Several shape analyses also tried to make good use of size information. In the development of the THOR
tool, Magill et al. [19] proposed an adaptive shape analysis where additional numerical analysis can be used
to help gain better precision. Its abstraction mechanism is also employed in C-to-gate hardware synthesis [20]. Magill et al. [21] formulated a novel instrumentation process which inserts numerical instructions
into programs, based on their shape analysis and user-provided predicates. Instrumented programs canthen be used to generate pure numerical programs for further analysis. Different from their work, we take
both shape and numerical information into consideration when performing the abstraction, and derive thenumerical abstraction from the shape constraint abstraction. Our approach can be more precise as we havemore information for the abstraction. Furthermore, we can directly handle data structures with stronger
invariants, like sortedness and height-balancedness, which have not been addressed in THOR, to the best of
our knowledge. For example, the append procedure used in quick sort (mentioned in Sec. 4.2 and Fig. 13)
cannot be handled in Magill et al. [21], probably due to the fact that their transformation from the original
program to its heap-free program may lose certain information (in this example the contents of the lists)
and that their analysis cannot transform the heap-free program back to the original program for further
analysis. While in our work, the discovered pure information is propagated back, and together with theheap specification, our analysis can verify the original program directly. Gulwani et al. [22] combine a set
domain with its cardinality domain in a general framework. Compared with these, our approach can handle
data structures with stronger invariants like sortedness, height-balanced and bag-related invariants, whichhave not been addressed in the previous works. Another piece of work, by Chang et al. [23] and Chang andRival [24], employs inductive checkers and checker segments to express shape and numerical information.
Our previous loop invariant synthesis [25] also infers strong loop invariants with both shape and numericalinformation but is limited to while loop analysis. Compared with their works, ours addresses specification
refinement with pure properties (including numerical and bag ones) in both pre- and postconditions byprocessing shape and pure information in two phases with the help of pure abduction. Our previous loop
invariant synthesis [25] also infers strong loop invariants with a one-phase heavyweight abstract interpretation. Compared with this work, it is limited to loop analysis, whereas this work tackles not only loops
but also methods; meanwhile this work is more lightweight as it solves the constraint abstraction in twophases where the second phase (pure constraint abstraction solving) utilises existing provers and is hence
more modular and efficient.
There are also many other approaches to expressing heap-based domains than separation logic. Hackett
and Rugina [26] can deal with AVL-trees but is customised to handle only tree-like structures with heightproperty. The shape analysis framework TVLA [27] is based on three-valued logic. It is capable of handlingcomplicated data structures and properties, such as sortedness. LRP [28] is fully decidable over multiple
linked data structures and has a finite model property. Guo et al. [29] reported a global shape analysis that
discover inductive structural shape invariants from the code. Kuncak et al. [30] developed a role system
to express and track referencing relationships among objects, where an object’s role (type) depends on,
and changes according to, the mutation of its referencing. Bouajjani et al. [31] automatically synthesize
invariants for list manipulating programs over infinite data domains using a graph representation of heap.
Compared with these works, a separation logic based approach benefits from the frame rule and hence
supports local reasoning. Meanwhile, our approach heads towards full functional correctness including bagrelated properties, which previous ones do not generally handle (except for [31] which captures various
aspects of data structures, such as the size, the sum or the multiset of linked list, relations of the data at
linearly ordered or successive positions).
Classical abstract interpretation [32] and its applications such as automated assertion discovery [33,34, 35, 36] mainly focus on finding numerical program properties. Our work is complementary to theseadvances as our focus is more on refining specifications for heap-manipulating programs. Meanwhile, we can23

utilise such works as our pure solver, for example the disjunction inference [10]. Semi-automatic approaches[37, 38] are also used to infer numerical constraints for given type templates in functional programs, wheredata structures are mostly immutable.
On the verification side, Smallfoot [39] is the first verification system based on separation logic. The
Hip/Sleek verification system [1, 2] supports user-defined shape predicates over the combined shape andnumerical domain. The Sleek tool has played a very important role in our analysis. The PALE system [40]transforms constraints in the pointer assertion logic (PAL) into monadic second-order logic (MSO) anddischarge them with MONA.JML [41] uses model/ghost fields and model methods to specify/model Java
program properties. Hob [42] is a modular program verification tool for shape properties. Based on Hob,
Jahob [43, 42] takes Java as its target language and allows more general specification language. Havoc [44]is another verification tool for the C language about heap-allocated data structures, using a novel reachability predicate. Dafny [45] translates programs into Boogie 2 [46] and conducts modular verification using
dynamic frames. There is another recent work on refining specifications via counterexample-guided abstraction refinement [47] which is goal-driven and incrementally improves the performance for given safety
requirements. Among these works, our verification is distinguished because we free users from writing whole
specifications by requiring only partial specifications, and omit user-supplied annotations for less important
loops and auxiliary methods.
6.2. Conclusion
We have reported a new approach to program verification that accepts partial specifications of methods,
and refines them by discovering missing constraints for numerical and bag properties, aiming at full functionalcorrectness for pointer-based data structures. We further augment our approach by requiring only partial
specification for primary methods. Specifications for loops and auxiliary methods can then be systematicallydiscovered. We have built a prototype system and the initial experimental results are encouraging.
References[1] H. H. Nguyen, W.-N. Chin, Enhancing program verification with lemmas, in: A. Gupta, S. Malik (Eds.), CAV, Vol. 5123
of Lecture Notes in Computer Science, Springer, 2008, pp. 355–369.
[2] H. H. Nguyen, C. David, S. Qin, W.-N. Chin, Automated verification of shape and size properties via separation logic, in:
B. Cook, A. Podelski (Eds.), VMCAI, Vol. 4349 of Lecture Notes in Computer Science, Springer, 2007, pp. 251–266.
[3] C. Calcagno, D. Distefano, P. W. O’Hearn, H. Yang, Compositional shape analysis by means of bi-abduction, Journal of
the ACM 58 (6) (2011) 26.
[4] D. Distefano, P. W. O’Hearn, H. Yang, A local shape analysis based on separation logic, in: H. Hermanns, J. Palsberg(Eds.), TACAS, Vol. 3920 of Lecture Notes in Computer Science, Springer, 2006, pp. 287–302.
[5] H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, Scalable shape analysis for systems code,in: 20th CAV, Vol. 5123 of LNCS, Springer, 2008, pp. 385–398.
[6] J. C. Reynolds, Separation logic: A logic for shared mutable data structures, in: 17th IEEE Symposium on Logic in
Computer Science (LICS 2002), IEEE Computer Society, 2002, pp. 55–74.
[7] S. S. Ishtiaq, P. W. O’Hearn, Bi as an assertion language for mutable data structures, in: Conference Record of the 28th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2001), 2001, pp. 14–26.
[8] J. Gustavsson, J. Svenningsson, Constraint abstractions, in: Programs as Data Objects II, Aarhus, Denmark, 2001, pp.
63–83.
[9] T. Nipkow, L. C. Paulson, M. Wenzel, Isabelle/HOL — A Proof Assistant for Higher-Order Logic, Vol. 2283 of LNCS,
Springer, 2002.
[10] C. Popeea, W.-N. Chin, Inferring disjunctive postconditions, in: M. Okada, I. Satoh (Eds.), ASIAN, Vol. 4435 of Lecture
Notes in Computer Science, Springer, 2006, pp. 331–345.
[11] T.-H. Pham, M.-T. Trinh, A.-H. Truong, W.-N. Chin, Fixbag: A fixpoint calculator for quantified bag constraints, in:
G. Gopalakrishnan, S. Qadeer (Eds.), CAV, Vol. 6806 of Lecture Notes in Computer Science, Springer, 2011, pp. 656–662.
[12] W.-N. Chin, C. David, H. H. Nguyen, S. Qin, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Science of Computer Programming 77 (2012) 1006–1036. doi:10.1016/j.scico.2010.07.004.
[13] W.-N. Chin, C. David, H. H. Nguyen, S. Qin, Automated verification of shape, size and bag properties, in: 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), IEEE Computer Society, 2007, pp.
307–320.
[14] M. Rubio-Sánchez, J. Urquiza-Fuentes, C. Pareja-Flores, A gentle introduction to mutual recursion, in: ITiCSE ’08:
Proceedings of the 13th annual conference on Innovation and technology in computer science education, ACM, New York,NY, USA, 2008, pp. 235–239.

24

[15] R. Barry, FreeRTOS reference manual: API functions and configuration options, Real Time Engineers Ltd.
http://www.freertos.org/ , 2009.
[16] A. Gotsman, J. Berdine, B. Cook, Interprocedural shape analysis with separated heap abstractions, in: K. Yi (Ed.), SAS,
Vol. 4134 of Lecture Notes in Computer Science, Springer, 2006, pp. 240–260.
[17] J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O’Hearn, T. Wies, H. Yang, Shape analysis for composite data
structures, in: W. Damm, H. Hermanns (Eds.), CAV, Vol. 4590 of Lecture Notes in Computer Science, Springer, 2007,
pp. 178–192.
[18] D. Distefano, Attacking large industrial code with bi-abductive inference, in: FMICS, 2009, pp. 1–8.
[19] S. Magill, J. Berdine, E. M. Clarke, B. Cook, Arithmetic strengthening for shape analysis, in: H. R. Nielson, G. Filé(Eds.), SAS, Vol. 4634 of Lecture Notes in Computer Science, Springer, 2007, pp. 419–436.
[20] B. Cook, A. Gupta, S. Magill, A. Rybalchenko, J. Simsa, S. Singh, V. Vafeiadis, Finding heap-bounds for hardware
synthesis, in: FMCAD, 2009, pp. 205–212.
[21] S. Magill, M.-H. Tsai, P. Lee, Y.-K. Tsay, Automatic numeric abstractions for heap-manipulating programs, in: M. V.
Hermenegildo, J. Palsberg (Eds.), POPL, ACM, 2010, pp. 211–222.
[22] S. Gulwani, T. Lev-Ami, M. Sagiv, A combination framework for tracking partition sizes, in: Z. Shao, B. C. Pierce (Eds.),
POPL, ACM, 2009, pp. 239–251.
[23] B.-Y. E. Chang, X. Rival, G. C. Necula, Shape analysis with structural invariant checkers, in: Static Analysis Symposium2007 (SAS’07), Denmark, 2007, pp. 384–401.
[24] B.-Y. E. Chang, X. Rival, Relational inductive shape analysis, in: G. C. Necula, P. Wadler (Eds.), POPL, ACM, 2008,
pp. 247–260.
[25] S. Qin, G. He, C. Luo, W.-N. Chin, Loop invariant synthesis in a combined domain, in: Proceedings of the 12th International Conference on Formal engineering methods and software engineering, ICFEM’10, Springer-Verlag, Berlin,
Heidelberg, 2010, pp. 468–484.
[26] B. Hackett, R. Rugina, Region-based shape analysis with tracked locations, in: J. Palsberg, M. Abadi (Eds.), POPL,
ACM, 2005, pp. 310–323.
[27] S. Sagiv, T. W. Reps, R. Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming
Languages and Systems 24 (3) (2002) 217–298.
[28] G. Yorsh, E. Rabinovich, M. Sagiv, A. Meyer, A. Bouajjani, A logic of reachable patterns in linked data-structures, in:
FOSSACS, 2006, pp. 94–110.
[29] B. Guo, N. Vachharajani, D. I. August, Shape analysis with inductive recursion synthesis, in: J. Ferrante, K. S. McKinley(Eds.), PLDI, ACM, 2007, pp. 256–265.
[30] V. Kuncak, P. Lam, M. C. Rinard, Role analysis, in: Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (POPL 2002), 2002, pp. 17–32.
[31] A. Bouajjani, C. Dragoi, C. Enea, A. Rezine, M. Sighireanu, Invariant synthesis for programs manipulating lists withunbounded data, in: 22nd International Conference on Computer Aided Verification, CAV 2010, Springer-Verlag, 2010,
pp. 72–88.
[32] P. Cousot, R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction
or approximation of fixpoints, in: Conference Record of the Fourth ACM Symposium on Principles of Programming
Languages (POPL 1977), ACM, 1977, pp. 238–252.
[33] P. Cousot, R. Cousot, On abstraction in software verification, in: Proceedings of the 14th International Conference on
Computer Aided Verification, Springer-Verlag, London, UK, 2002, pp. 37–56.
[34] A. Gupta, R. Majumdar, A. Rybalchenko, From tests to proofs, in: TACAS ’09: Proceedings of the 15th International
Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer-Verlag, Berlin, Heidelberg,
2009, pp. 262–276.
[35] A. Gupta, A. Rybalchenko, Invgen: An efficient invariant generator, in: A. Bouajjani, O. Maler (Eds.), CAV, Vol. 5643
of Lecture Notes in Computer Science, Springer, 2009, pp. 634–640.
[36] S. Srivastava, S. Gulwani, Program verification using templates over predicate abstraction, in: PLDI, 2009, pp. 223–234.
[37] P. M. Rondon, M. Kawaguchi, R. Jhala, Liquid types, in: R. Gupta, S. P. Amarasinghe (Eds.), PLDI, ACM, 2008, pp.
159–169.
[38] M. Kawaguchi, P. M. Rondon, R. Jhala, Type-based data structure verification, in: M. Hind, A. Diwan (Eds.), PLDI,
ACM, 2009, pp. 304–315.
[39] J. Berdine, C. Calcagno, P. W. O’Hearn, Smallfoot: Modular automatic assertion checking with separation logic, in: F. S.
de Boer, M. M. Bonsangue, S. Graf, W. P. de Roever (Eds.), FMCO, Vol. 4111 of Lecture Notes in Computer Science,
Springer, 2005, pp. 115–137.
[40] A. Möller, M. I. Schwartzbach, The pointer assertion logic engine, ACM SIGPLAN Notices 36 (5) (2001) 221–231.
[41] L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, E. Poll, An overview of JML
tools and applications, International Journal on Software Tools for Technlogy Transfer 7 (3) (2005) 212–232.
[42] T. Wies, V. Kuncak, K. Zee, A. Podelski, M. C. Rinard, On verifying complex properties using symbolic shape analysis,
CoRR abs/cs/0609104.
[43] V. Kuncak, Modular data structure verification, Ph.D. thesis, EECS Department, Massachusetts Institute of Technology(February 2007).
[44] S. Chatterjee, S. K. Lahiri, S. Qadeer, Z. Rakamaric, A reachability predicate for analyzing low-level software, in: TACAS,
2007, pp. 19–33.
[45] K. R. M. Leino, Dafny: An automatic program verifier for functional correctness, in: E. M. Clarke, A. Voronkov (Eds.),
LPAR (Dakar), Vol. 6355 of Lecture Notes in Computer Science, Springer, 2010, pp. 348–370.

25

[46] K. R. M. Leino, P. Rümmer, A polymorphic intermediate verification language: Design and logical encoding, in: J. Esparza,
R. Majumdar (Eds.), TACAS, Vol. 6015 of Lecture Notes in Computer Science, Springer, 2010, pp. 312–327.
[47] M. Taghdiri, Automating modular verification by refining specifications, Ph.D. thesis, EECS Department, Massachusetts
Institute of Technology (Feburary 2008).

Appendix A. Shape Predicate Definitions
Below are the definitions of the shape predicates which are used in the experiments but not given in
paper:ls(root, p, n) ≡(root=p ∧ n=0) ∨ (root7→node( , q)∗ls(q, p, m) ∧ n=m+1)
dll(root, p, n) ≡(root=p ∧ n=0) ∨(root7→node2(v, p, q)∗dll(q, root, n1 ) ∧ n=n1 +1)
dllB(root, p, S) ≡(root=p ∧ S=∅) ∨(root7→node2(v, p, q)∗dllB(q, root, S1 ) ∧ S=S1 ⊔{v})
sll(root, n, mn, mx) ≡(root=null ∧ n=0 ∧ mn=mx) ∨(root7→node(v, q)∗sll(q, n1 , k, mx) ∧ n=n1 +1 ∧ mn≤k)
sllB2(root, S) ≡(root=null ∧ S=∅) ∨(root7→node(v, q)∗sllB2(q, S1 ) ∧ S={v}⊔S1 ∧ (∀x∈S1 ·v≥x))
slsB(root, p, S) ≡(root=p ∧ S=∅) ∨(root7→node(v, q)∗slsB(q, p, S1 ) ∧ S={v}⊔S1 ∧ (∀x∈S1 ·v≤x))bt(root, S, h) ≡(root=null ∧ S=∅ ∧ h=0)∨(root7→node2(v, p, q)∗bt(p, Sp , hp )∗bt(q, Sq , hq ) ∧ S=Sp ⊔Sq ∧ h=1+max(hp , hq ))bst(root, mn, mx) ≡(root=null ∧ mn=mx) ∨(root7→node2(v, p, q)∗bst(p, mn, mxl)∗bst(q, mnr , mx) ∧ mxl ≤v≤mnr )bstB(root, S) ≡(root=null ∧ S=∅) ∨(root7→node2(v, p, q)∗bstB(p, Sp )∗bstB(q, Sq )∧S={v}⊔Sp ⊔Sq ∧ ∀vp ∈Sp , vq ∈Sq · vp ≤v≤vq )avl(root, S, h) ≡(root=null ∧ S=∅ ∧ h=0)∨(root7→node2(v, p, q)∗avl(p, Sp , hp )∗avl(q, Sq , hq )∧S=Sp ⊔Sq ∧ h=1+max(hp , hq ) ∧ −1≤hp −hq ≤1)
rbt(root, S, c, h) ≡(root=null ∧ S=∅ ∧ c=0 ∧ h=0) ∨(root7→node2(v, p, q)∗rbt(p, Sp , cp , hp )∗rbt(q, Sq , cq , hq )∧S=Sp ⊔Sq ∧ ((c=0 ∧ h=hp +1 ∧ hp =hq ) ∨ (c=1 ∧ cp =cq =0 ∧ h=hp =hq ))Note: c=0 denotes the color of the node is black and c=1 denotes a red node.

26