Automatically Refining Partial Specifications
for Program Verification ⋆Shengchao Qin1 , Chenguang Luo2 , Wei-Ngan Chin3 , and Guanhua He1,2
1

Teesside University 2 Durham University 3 National University of Singapore
Abstract. Automatically verifying heap-manipulating programs is achallenging task, especially when dealing with complex data structureswith strong invariants, such as sorted lists and AVL/red-black trees. The
verification process can greatly benefit from human assistance throughspecification annotations, but this process requires intellectual effort
from users and is error-prone. In this paper, we propose a new approachto 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 revised by users. We further
augment our approach by requiring only partial specification to be given
for primary methods. Specifications for loops and auxiliary methods canthen be systematically discovered by our augmented mechanism, withthe help of information propagated from the primary methods. Our workis aimed at verifying beyond shape properties, with the eventual goal ofanalysing full functional properties for pointer-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.

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 be analysed may be complicated and with significant diversity.
Therefore, it may be unreasonable to expect user to provide specification forevery method and invariant for every loop when verifying larger software systems.
Furthermore, to err is human. A programmer may under-specify with too weaka precondition or over-specify with too strong a postcondition. Such mistakes
could lead to failed verification, and it may be difficult to distinguish between areal bug or an inappropriate annotation.
⋆

This work is supported in part by EPSRC project EP/G042322 and MoE ARF grantR-252-000-411-112.

2

S. Qin, C. Luo, W.-N. Chin and G. He

To balance verification quality and human effort, we provide a novel approach to the verification of heap manipulating programs, which has long since
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 numerical information (size 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 rest of the work to refine thosepartial specifications with derived (pure) constraints which should be satisfied
by the program, or report a possible program bug if the given specifications are
rejected by our verifier. This is an improvement over previous works [23], whereusers must provide full specifications for each method and invariants for eachloop. This is also significantly different from the compositional shape analysis [5,9, 32]. In spite of a higher level of automation, their analysis focuses on pointersafety only and deals primarily with a few built-in predicates over the shapedomain only. Our work targets at both memory safety and functional correctness and supports user-defined predicates over several abstract domains (suchas 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 (as in [5, 9]):list(p) ≡ (p=null)∨(∃i, q · p7→node(i, q)∗list(q))
Note that in the inductive case, the separation conjunction ∗ ([28]) ensures that
two heap portions (the head node and the tail list) are domain-disjoint.
Yet another user may be interested to track also the length of a list to analyse
quantitative measures, such as heap/stack resource usage, usingll(p, n) ≡ (p=null∧n=0)∨(p7→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 multi-set (bag) property:llB(p, S)≡(p=null∧S=∅)∨(p7→node(v, q)∗llB(q, S1 )∧S={v}⊔S1 )where the length of the list is implicitly captured by the cardinality |S|. A further
strengthening can capture also the sortedness property:sllB(p, S)≡(p=null∧S=∅)∨(p7→node(v, q)∗sllB(q, S1 )∧S={v}⊔S1 ∧(∀x∈S1 ·v≤x))
Therefore, the user can provide predicate definitions w.r.t. various correctnesslevel and program properties, which can be as simple as normal lists or as complicated as AVL trees, depending on their requirements. These predicates are
non-trivial but can be reused multiple times for specifications of different methods. We have also built a library of predicates with respect to commonly-useddata structures and useful program properties.

Automatically Refining Partial Specifications for Program Verification

3

Based on these predicates, the user is expected to provide partial specifications for some primary methods which are the main objects of verification.
Say, for a sorting algorithm taking x as input parameter that is expected to be
non-null, the user may provide llB(x, S1 ) as precondition and sllB(x, S2 ) as postcondition, and our approach will refine the specification as llB(x, S1 ) ∧ x6=null
for pre, and sllB(x, S2 ) ∧ S1 =S2 for post. Here we need user annotations as theinitial specification, because we reserve the flexibility of verification w.r.t. different program properties at various correctness levels. For example, our approach
can verify the same algorithm, but for different refined specifications, such as:
requires list(x) ∧ x6=null ensures list(x)ensures ll(x, n2 ) ∧ n1 =n2
requires ll(x, n1 ) ∧ n1 >0
requires llB(x, S1 ) ∧ x6=null ensures llB(x, S2 ) ∧ S1 =S2
requires llB(x, S) ∧ x6=null ensures ll(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 human’s insights and machine’s capability at automated program analysis. In particular, human’s guidance can help narrow downon the most important of the different specifications that are possible with eachprogram code, while automation by machine is important for minimising on thetedium 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 formemory 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 to verify, so as to provide different levels of correctness.
Meanwhile we aim at, and have covered much of, full functional correctnessof 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 reduce users’ annotations. As for our experiments, theuser only has to supply the partial specifications for primary methods, andthe analysis will compute pre- and postconditions for loops and auxiliary
methods as well as refine primary methods’ specifications.
– Semi-Automation: We classify our approach as semi-automatic, because theuser is allowed to interfere and guide the verification at any point. For instance, they may provide invariant for a loop instead of our automated invariant generation, or choose some other constraints as refinement from what
the verification has discovered.
We have built a prototype implementation and carried out a number of experiments to confirm the viability of the approach as described in Section 5. In what
follows, we will first depict our approach informally using a motivating example and present technical details thereafter. More related works and concluding
remarks come after the experimental results.Technical details not covered here
can be found in our report [27].

4

S. Qin, C. Luo, W.-N. Chin and G. He

2Illustrative Example

We illustrate our approach with an example. We show how our analysis infers
missing constraints to improve the user-supplied incomplete specification, andhow it analyses the while loop without user-annotations.
0 data node2 { int val; node2 prev; node2 next; }9
end=end.next; root=root.next;}
1 node2 sdl2nbt(node2 head,
10 }node2 tail)11 if (head == root) root.prev = null;
2 requires sdlB(head, p, q, S)
12 else root.prev = sdl2nbt(head,root);
3 ensures nbt(res, Sres )13 node2 tmp = root.next;
4 {node2 root = head;
14 if (tmp == tail) root.next = null;
5 node2 end = head;
15 else { tmp.prev = null;
6 while(end != tail) {16
root.next = sdl2nbt(tmp, tail);}7
end = end.next;
17 root;}8
if (end != tail) {Fig. 1. The method to convert a sorted doubly-linked list to a node-balanced tree.

The method sdl2nbt (Fig 1) converts
t
o
o
r
d
n
e
d
a
e
h
a doubly-linked sorted list into a nodel
l
u
n
1
2
3
4
5
6
l
i
a
t
balanced binary search tree, as indicated
(a)
t
o
o
r
t
o
o
r
by the shape-only specification in lines 2
44
and 3. It first finds the “centre” node in262
6
the list (root), where the difference be1
3
5
1
3
5
tween numbers of nodes to the left and to(b)(c)
the right of the centre node is at most one
Fig. 2. sdl2nbt(lines 5-10), as Fig 2 (a) shows. It then applies the algorithm recursively on both list segments to the left and to the rightof the centre node, and regards the centre node as the tree’s root, whose left
and right children are the resulted subtrees’ roots from the recursive calls (lines
11-17), as in Fig 2 (b) and (c). As the data structures of doubly-linked list andbinary 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 in line
1 denotes the first node of the input list, and tail is where the last node’s next
field points to. When using this method tail should be set as null initially.
The predicate for doubly-linked sorted list (segment) is defined as follows:sdlB(root, p, q, S) ≡ (root=q ∧ S=∅) ∨ (root7→node2(v, p, r) ∗sdlB(r, root, q, S1 ) ∧ root6=q ∧ S={v} ⊔ S1 ∧ (∀x∈S1 ·v≤x))where the parameters p and q denote resp. the prev field of root and the next
field of the last node in the list, and S represents the list’s content. And below
is the predicate specification for node-balanced binary search trees: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 right sub-trees be within one, as the node-balanced
property indicates.

Automatically Refining Partial Specifications for Program Verification

5

To refine sdl2nbt’s specification, our analysis proceeds in two steps. Firstly,
starting from the partial precondition (line 2 of Fig 1), a forward analysis isconducted to compute the postcondition of the method in the form of a constraint
abstraction [15]. This constraint abstraction is effectively a transfer function forthe method, which may be recursively defined (e.g. in this example). Secondly,
instead of a direct fixpoint computation in the combined abstract domain (withshape, numerical and bag information), a “pure” constraint abstraction (without
heap shape information) is derived from the generated constraint abstraction andthe user-given partial postcondition. This pure constraint abstraction is thensolved by fixpoint solvers in pure (numerical/bag) domains, such as [24, 25].
As for the example, when the forward analysis reaches the while loop at line
6, it discovers that the loop has no user-supplied annotations. In that case, it uses
an augmented technique (details follow slightly later) to synthesise the loop’s preand post-shapes, and invoke the analysis procedure recursively to find additional
pure constraints. In this way, we can infer the while loop’s postcondition assdlB(head, null, root, Sh ) ∗ sdlB(root, p, tail, Sr ) ∧(1)
end=tail ∧ S=Sh ⊔Sr ∧ (∀x∈Sh , y∈Sr ·x≤y) ∧ 0≤|Sr |−|Sh |≤1which indicates that the original list starting from head is cut into two sorted
pieces with a cutpoint root. Meanwhile, the essential constraint (the underlinedpart, 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:
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, resh , 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 some logical 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 instantiations of the parameters).
During this process, all occurrences of Q are replaced by the post-shape conjoinedwith 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 [23]) are used to form (via disjunction) the definition of P:

6

S. Qin, C. Luo, W.-N. Chin and G. He

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 fieldshould be null, and the whole list’s last node’s next field must point to tailfor 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
Analysis for the while loop. The while loop in sdl2nbt (lines 6-10) discovers
the centre node of the given list segment referenced by head. 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- andpost-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 theloop starts. The post-shape synthesis is done by checking the symbolic execution result of the loop body (unrolled once) against possible abstracted 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 bodyis 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 ∨(2)
head7→node2(vh , p, root) ∗ root7→node2(vr , head, end) ∧ end=tailwhere (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 postshape, we can employ the same approach to generate a constraint abstraction
for the while loop, and solve it to obtain formula (1) in page 5.

3

Language and Abstract Domain

We focus on a strongly-typed C-like imperative language in Fig 3. 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 language is expression-oriented, so the body of a method is an expression
1

We will explain how to attach the fixpoint result to both pre and post in Sec 4.

Automatically Refining Partial Specifications for Program Verification

7

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

composed of e (the recursively defined program constructor) and d and d[v] (atominstructions/expressions). We also allow both call-by-value and call-by-reference
method parameters (which are separated with a semicolon ;).
spred ::= pred(v ∗ ) ≡ Φmspec ::= requires Φpr ensures Φpo∗∆::= Q(v
W ) | Φ | ∆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 · φb::= true | false | v | b1 = b2
a ::= s1 =s2 | s1 ≤s2s::= kint | v | kint ×s | s1 +s2 | −s | max(s1 ,s2 ) | min(s1 ,s2 ) | |B|ϕ::= v∈B | B1 =B2 | B1 <B2 | B1 ⊑B2 | ∀v∈B·φ | ∃v∈B·φ
B::= B1 ⊔B2 | B1 ⊓B2 | B1 −B2 | {} | {v}Fig. 4. The Specification Language.

Our specification language (in Fig 4) allows (user-defined) shape predicatesto specify both separation and pure properties. The shape predicates spred are
constructed with disjunctive constraints Φ. We require that the predicates bewell-formed [23]. A conjunctive abstract program state, σ, is composed of a heap
(shape) part κ and a pure part π, where π consists of γ, φ and ϕ as aliasing,numerical and bag information, respectively. We use SH to denote the set ofsuch conjunctive states. During the symbolic execution, the abstract program
state at each program point will be a disjunction of σ’s, denoted by ∆. Notethat 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 [23]. Pure constraint abstraction P is analogously defined to Q.
Our memory model is adapted from that of separation logic [28], except that
we consider memory cells to be structured records. The detailed model definitions
can be found in Nguyen et al. [23]. Meanwhile, for program variables in abstractstates, we use unprimed ones to denote their initial values and primed ones for
current values [23, 27].

4

The Analysis

In this section, we first formulate the main analysis for (primary) methods
with given shape specifications. We then show how the analysis is extended tohandle auxiliary methods (including loops) without user annotations.

8

4.1

S. Qin, C. Luo, W.-N. Chin and G. He

Refining Specifications for Primary Methods

The algorithm for refinement (CA Gen Solve) is given in Fig 5. As illustrated
in Section 2, the analysis proceeds in two steps for a primary method with shapeinformation given in specification, namely (1) forward analysis (at lines 1-2) and(2) pure constraint abstraction generation and solving (at lines 3-10).
Algorithm CA Gen Solve(T , mn, e, Φpr ,Φpo ,u∗ ,v ∗ )1∆ := Symb Exec(T , mn, e, Φpr )2
if ∆ = fail then return fail end if
W
3
Normalise ∆ to DNF, and denote as mi=1 ∆i∗∗ ∗ ′∗∗ ∗ ′∗
4
w :={u ,v ,v } ∪ pureV({u ,v ,v }, Φpr ∨Φpo )W
5∆P := Pure CA Gen(Φpo , Q(w∗ )::= mi=1 ∆i )6
if ∆P = fail then return fail end if
7
π := Pure CA Solve(P(w∗ )::=∆P )8
R := t mn ((t u)∗ ; (t v)∗ ) requires!
ex quan(Φpr , π) ensures ex quan(Φpo , π)9if Verify(T , mn, R) then return T ∪ {R} \! { t mn ((t u)∗ ; (t v)∗ ) requires Φpr ensures Φpo }10else return fail end if
end Algorithm

Algorithm Symb Exec
! (T , mn, e, Φpr )11 errLbls := ∅12 do
13 (∆, l) := |[e]|mnT (Φpr , 0)
14 if l>0∧l∈errLbls
/
then
15
Φpr :=ex quan(Φpr ,∆);
16
errLbls := errLbls ∪{l}17 else if l>0 ∧ l∈errLbls! then return fail18 end if
19 while l > 0
20 return ∆end Algorithm

Fig. 5. Refining method specifications.

The forward analysis is captured as algorithm Symb Exec to the right ofFig 5. Starting from a given pre-shape Φpr , it analyses the method body e tocompute the post-state in constraint abstraction form. Due to space constraints,
the symbolic execution rules are given in our technical report [27]. They are
similar to symbolic rules used in [23], except for a novel mechanism to derive
pure precondition, which we refer to as pure abduction.
This pure abduction mechanism is invoked whenever symbolic execution fails
to prove memory safety based on the current prestate. For example, if the current
state is ll(x, n) (a list that is possibly empty) but x7→node( , p) is required by
the next program instruction, our pure abduction mechanism will infer n≥1
to add to the current state to satisfy the requirement. The variable errLbls(initialised at line 11) is to record the program locations in which previous pureabductions occurred. Whenever the symbolic execution fails, it returns a state∆ that contains the pure abduction result and the location l where failure was
detected, as shown in line 13. If the current abduction location l is not recordedin 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 thealgorithm 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 a previous failure point was re-encountered.
The latter may indicate a program bug or a specification error, or may be dueto the possible incompleteness of the underlying Sleek prover we use.
Back to the main algorithm CA Gen Solve, the analysis next builds a heapbased constraint abstraction mechanism, named Q(w∗ ), for the post-state in steps
3-4. This constraint abstraction is possibly recursive. (Definition † in page 5 is anAutomatically Refining Partial Specifications for Program Verification

9

example of this heap-based abstraction.) We then make use of another algorithm
in Fig 6, named Pure CA Gen, to extract a pure constraint abstraction, namedP(w∗ ), without any heap property. (Definition ‡ in page 6 is an instance of thispure abstraction.) This algorithm tries to derive a branch Pi for each branch∆i of Q. For every ∆i it proceeds in two steps. In the first step (lines 22-24), it
replaces the recursive occurrence of Q in ∆i with σ ∗ P(w∗ ). In the second step(lines 25-26) it tries to derive Pi via the entailment. If the entailment fails, thenpure 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. [25]) 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 in line 8, before
we perform a post verification in line 9 using the Hip verifier [23], to ensure thestrengthened 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 Φprand Φpo are added into the parameter list of the constraint abstraction Q. The
function ex quan(∆, π) is to strengthen the state ∆ with the 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) returns ll(x, n) ∧ 0<n.
W
Algorithm Pure CA Gen(σ, Q(w∗ )::= mi=1 ∆i )21 for i = 1 to m
22
Denote all appearances of Q(w∗ ) in ∆i as Qj (wj∗ ), j = 1, ..., p23
Denote substitutions ρj = [([wj∗ /w∗ ]σ ∗ P(wj∗ ))/Qj (wj∗ )]24
Let substitution ρ := ρ1 ◦ ρ2 ◦ ... ◦ ρp as applying all substitutions!
defined above in sequence25
if (ρ∆i ⊢ σ ∗ σi or ρ∆i ∧ [σi′ ]  σ ∗ σi ) and ispure(σi ) then Pi := σi26else return fail end if
27 end forW
28 return m
i=1 Piend Algorithm
Fig. 6. Pure constraint abstraction generation algorithm.

Pure abduction mechanism. We use the Sleek prover [23] to check ∆1 entails ∆2 . If the entailment holds it also derives the frame ∆3 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 7) to discover
missing pure constraints σ ′ 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. in ll(x, n) 0 x7→node( , null),the RHS can entail the LHS with pure frame n=1. The abduction then checks to10

S. Qin, C. Luo, W.-N. Chin and G. He

ensure ll(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.
σ 0 σ1 ∗ trueσ1 ⊢ σ ∗ σ ′ispure(σ ′ )σ ∧ σ ′ ⊢ σ1 ∗ σ2
(R1)

σ ∧ [σ ′ ]  σ1 ∗ σ2

σ 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(σ ′ )(R2)σ ∧ σ ′ ⊢ σ1 ∗ σ2σ ∧ [σ ′ ]  σ1 ∗ σ2

(R3)

Fig. 7. Pure abduction rules.

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 on the LHS are of disjunctive forms (i.e. sllB in σ),
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, theabduction returns |S|=2 (σ ′ ) and discovers the nontrivial frame S={u, v} ∧ u≤v(σ2 ). Note that function data no returns the number of data nodes in a state,e.g. it returns one for x7→node(v, p) ∗ ll(p, m). (This syntactic check is important
for the termination of the abduction.) The unroll operation unfolds
Wu all shapepredicates once in σ, normalises the result to a disjunctive form ( i=1 σ i ), andreturns the result as a set of formulae ({σ 1 , ..., σ u }).
In the third rule (R3), neither side entails the other and the LHS term cannot
be unfolded. e.g., σ = x7→node(u, p) ∗ p7→node(v, null), σ1 = ∃S · sllB(x, S). In
this case, the rule swaps the two sides of the entailment and applies the second
rule to uncover the pure 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).
4.2

Inferring Specifications for Auxiliary Methods and Loops

For auxiliary methods2 , we conduct a pre-analysis (Fig 8) to synthesise thepre- and post-shapes before we conduct the refinement analysis from Fig 5. Loops
are dealt with by analysing their tail-recursive versions in the same way. Thisapproach alleviates the need for users to provide specification annotations forboth loops and auxiliary methods.
The pre-shape synthesis algorithm SynPre (Fig 8 left) takes in as input the setof 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 first obtains
possible shape candidates from the parameters u∗ , v ∗ with ShpCand (line 1),
2

In practice, we treat methods without user-specified shape specifications as auxiliary.

Automatically Refining Partial Specifications for Program Verification
Algorithm SynPre∗∗∗∗! (S, f, u , v , σ, x , y )1 C := ShpCand(S, u∗ , v ∗ )2 for σC ∈ C do
3 if σ 0 [x∗ /u∗ , y ∗ /v ∗ ]σC
4 then C:=C\{σC } end if
5 end for6 return C
end Algorithm

11

Algorithm SynPost (T , S, f, e, Φpr , u∗ , v ∗ )7 C := ShpCand(S, u∗ , v ∗ )8 T ′ :=T ∪{f (u∗ ,v ∗ ) requires Φpr ensures false {e}}9 ∆ := Symb Exec(T ′ , f, syn unroll(f, e), Φpr )10 for σC ∈ C do
11
if ∆∧[σ] ⋫ σC then C := C\{σC } end if
12 end for
13 return pair spec list(Φpr , C)
end Algorithm

Fig. 8. Shape synthesis algorithms.

then picks up a sound abstraction for the method’s pre-shape with entailment,
and filter out the ones which fail (line 4). Finally the pre-shape abstraction is returned. While we use an enumeration strategy here, the number of possible shapecandidates 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.
To synthesise post-shapes (SynPost, Fig 8 right), we also assign C as possible shape candidates (line 7). 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 9), assuming f has a specification requires Φpr ensures false (line 8). The postcondition false is used to ensure that the execution only considers the effect ofthe program branches with no recursive calls (to f itself). We then use ∆ tofind out appropriate abstraction of post-shape (line 11), which is paired with
Φpr and returned as result. Here we use pure abduction to filter post-shapes topreserve as many shapes that are potentially refinable as possible. The function pair spec list(Φpr , C) forms an ordered list of pre-/post-shape pairs, each ofwhich 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 typenode, and two compatible shape predicates llB and sllB, 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 4 in Fig 8 left and line 11 in Fig 8 right) wheremost elements should be reduced because they are not sound abstractions. For
example, in the previous list, only llB(x, S) ∗ llB(y, T) remains in the list andparticipates in further verification.
The initial experimental results confirm that our shape synthesis keeps only
highly relevant abstractions. For the while loop in Section 2, we filtered out
24 (of 26) abstractions. Generally, in case that there are several abstractions
as candidate specifications, we employ some other mechanisms to reduce themfurther. Firstly, we prioritise post-shapes with same (or stronger) predicates as inprecondition since it is more likely that 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
the synthesised pre/post-shapes (to complete specifications). We retrieve (andremove) the pre/post-shape pair from the head of the list, (1) use the refinement

12

S. Qin, C. Luo, W.-N. Chin and G. He

algorithm (Fig 5) to obtain a specification for the auxiliary method, and (2)continue the analysis for the primary method. If the analysis for the primarymethod succeeds, we will ignore all other synthesised pre/post-shapes from thelist. These mechanisms help to keep attempts over candidate specifications at aminimum level.
Soundness. Based on the soundness of the following: the entailment prover [23],the abstract semantics (w.r.t. the concrete semantics), the pure constraint abstraction generation, and the fixpoint calculation [24, 25], we have
Theorem 1 (Soundness). Our analysis is sound with respect to the underlying
operational semantics.
The proof and more details can be found in the technical report [27].

5Experiments and Evaluation

We have implemented a prototype system for evaluation. Our experimental
results were achieved with an Intel Core 2 CPU 2.66GHz with 8Gb RAM. The
four columns in Fig 9 describe, resp., the analysed programs, the analysis timein seconds, and the primary methods’ (given and inferred) preconditions andpostconditions. All formulae with a grey background are inferred by our analysis. For some programs, we have verified them with different pre/post shape
templates. More results and details are available in the report [27].
The results highlight the refinement of both pre- and postconditions basedon user-provided shape specifications, even for complicated data structures suchas AVL and red-black trees. Firstly, our approach can compute non-trivial pureconstraints for postcondition, e.g. for delete we know the content of the result
list is subsumed by that of the input list, for list-sorting algorithms we confirm
the content of the output is the same as that of the input, and for tree-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 functionalcorrectness. As an example, the travrs method, taking in a list with length mand an integer n, traverses towards the tail of the list for n steps. the analysis
discovers m≥n in the precondition to ensure memory safety. Another example
is the append method concatenating two sorted lists into one. To ensure thatthe 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 a list,
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 sort

Automatically Refining Partial Specifications for Program Verification
Prog. Time Pre
List processing programs
0.591 ll(x, n) ∧ n≥1
sort
insert 0.504 sll(x, n, xs, xl)∧ v≥xs

ll(x, m) ∧ m=n+1

rand
insert0.522 ll(x, n) ∧ n≥1ll(x, m) ∧ m=n+1—

sll(x, m, mn, mx)∧ (fail)delete1.024 sllB(x, S) ∧ |S|≥2

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

travrs

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

sll(x, n, xs, xl)∧ (fail)

13

Post

sll(x, m, mn, mx)∧ xs=mn∧mx=max(xl,v)∧m=n+10.512 ll(x, xn)∗ll(y, yn)∧ xn≥1 ll(x, m) ∧ m=xn+yn
appendsll(x, xn, xs, xl)∧ xl≤ys
sll(x, m, rs, rl) ∧ yl=rl ∧ m≥1+yn ∧ m=xn+yn∗ sll(y, yn, ys, yl)
Sorting (main) llB(x, S) ∧ |S|≥1
sllB(res, T) ∧ T=S
(⋆)

merge

0.948

4.107 sllB(x, Sx ) ∗ sllB(y, Sy )sllB(res, T) ∧ T=Sx ⊔Syflatten 2.693 bstB(x, S)
sllB(res, T) ∧ T=S
Binary tree, binary search tree, AVL tree and red-black tree processing programs
insert 1.276 bt(x, S, h) ∧ |S|≥1 ∧ h≥1 bt(x, T, k) ∧ T=S⊔{v} ∧ h≤k≤h+1
delete0.970 bt(x, S, h) ∧ |S|≥2 ∧ h≥2 bt(x, T, k) ∧ ∃a.S=T⊔{a} ∧ h−1≤k≤hsearch

1.583 bst(x, sm, lg)

bst
insert1.720 bst(x, sm, lg)

avl ins 11.12 avl(x, S, h)
rbt ins

8.76 rbt(x, S)bst(x, mn, mx) ∧ sm=mn ∧ lg=mx ∧ 0≤res≤1bst(x, mn, mx) ∧ (v<sm∧v=mn∧lg=mx∨
lg<v∧v=mx∧sm=mn ∨ sm=mn∧lg=mx)
avl(res, T, k) ∧ T=S⊔{v} ∧ h≤k≤h+1
rbt(res, T) ∧ T=S⊔{v}

Fig. 9. Selected Experimental Results.

and flatten for tree sort) and their discovered specifications. Note that these
sorting algorithms have the same specification for their primary methods (line⋆). As another example, avl ins also has some auxiliary (recursive) methods
such as calculation of tree’s height, which are automatically analysed as well.
We have also tried our approach over part of the FreeRTOS kernel [2]. 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, whichfurther confirms the viability of our approach.

6

Related Work and Conclusion

Related works. The local shape analysis [9] infers loop invariants for listprocessing programs, followed by the SpaceInvader tool to verify larger industrial
codes [5, 32]. Gulavani et al. [12] propose a stronger bi-abduction algorithm tocompute the shape pre/post-condition at the same time. The SLAyer tool [11]implements an interprocedural shape analysis. To infer also size information,
THOR [19, 20] is armed with additional numerical analysis to gain better precision. Gulwani et al. [13] combine a set domain with its cardinality domain
in a general framework. Magill et al. [21] instrument programs with numeri-

14

S. Qin, C. Luo, W.-N. Chin and G. He

cal instructions from which pure numerical programs are generated for further
analysis. Compared with these, our approach can handle additional data structures with stronger invariants like sortedness, height-balanced and bag-related
invariants. Relational inductive shape analysis [6] employs inductive checkers to
express shape and numerical information, where they only demonstrate how toanalyse a program with one particular shape. Our previous loop invariant synthesis [26] also infers strong loop invariants. Compared with them, this work isinter-procedural and addresses specification refinement with pure properties inboth pre- and postconditions in two phases (for shape and pure resp.) with pureabduction.
There are also other approaches to expressing heap-based domains than separation logic. Hackett and Rugina [16] can deal with AVL-trees but is customised
to handle only tree-like structures with height property. TVLA [30] can handle
complicated data structure properties like sortedness. Bouajjani et al. [3] synthesise list-related invariants over infinite data domains using graph heap representation. Comparatively, separation logic based approach benefits from theframe rule and local reasoning. Meanwhile, our approach aims at full functionalcorrectness including both quantitative and content properties of shapes.
Automated assertion discovery techniques [8, 14, 31] mainly find numericalprogram properties. Our work is complementary to them as we focus more
on refining specifications for heap-manipulating programs. Semi-automatic approaches [17, 29] are also used to infer numerical constraints for given type templates in functional programs, where data structures are mostly immutable.
On the verification side, the Hip/Sleek verification system [23] supports
user-defined shape predicates over a combined domain. The PALE system [22]transforms constraints in the pointer assertion logic (PAL) into monadic secondorder logic (MSOL) and discharge them with MONA. JML [4] uses model/ghost
fields and model methods to specify/model Java program properties. Jahob [18]also verifies Java and focuses more on heap shape. Spec# [1] is for C# by enforcing object invariants and method specifications. Havoc [7] is another verification
tool for C language about heap-allocated data structures, using a novel reachability predicate. Compared with these works, we can free users from writing whole
specifications by requiring only partial specifications, and omit annotations forloops and auxiliary methods.
Concluding remarks. 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 approachby requiring only partial specification for primary methods. Specifications forloops and auxiliary methods can then be systematically discovered. We havebuilt a prototype system and the initial experimental results are encouraging.

References
1. M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system:
An overview. In CASSIS, 2004.
2. R. Barry. FreeRTOS — a free RTOS for small embedded real time systems. 2006.

Automatically Refining Partial Specifications for Program Verification

15

3. A. Bouajjani, C. Dragoi, C. Enea, A. Rezine, and M. Sighireanu. Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. In CAV, 2010.
4. L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. Leavens, K. Leino. An
Overview of JML Tools and Applications. STTT. 7(3):212–232. 2005.
5. C. Calcagno, D. Distefano, P. O’Hearn, and H. Yang. Compositional shape analysis
by means of bi-abduction. In POPL, 2009.
6. B. Chang and X. Rival. Relational inductive shape analysis. In POPL, 2008.
7. S. Chatterjee, S. Lahiri, S. Qadeer, and Z. Rakamaric. A reachability predicate foranalyzing low-level software. In TACAS, 2007.
8. P. Cousot and R. Cousot. On abstraction in software verification. In CAV, 2002.
9. D. Distefano, P. O’Hearn, and H. Yang. A local shape analysis based on separation
logic. In TACAS, 2006.
10. R. Giacobazzi. Abductive analysis of modular logic programs. In ILPS, 1994.
11. A. Gotsman, J. Berdine, and B. Cook. Interprocedural shape analysis with separated heap abstractions. In SAS, 2006.
12. B. Gulavani, S. Chakraborty, G. Ramalingam, and A. Nori. Bottom-up shapeanalysis. In SAS, 2009.
13. S. Gulwani, T. Lev-Ami, and M. Sagiv. A Combination Framework for Tracking
Partition Sizes. In POPL, 2009.
14. A. Gupta, R. Majumdar, and A. Rybalchenko. From tests to proofs. In TACAS09.
15. J. Gustavsson and J. Svenningsson. Constraint abstractions. In Programs as Data
Objects II, Denmark, May 2001.
16. B. Hackett and R. Rugina. Region-based shape analysis with tracked locations. In
POPL, 2005.
17. M. Kawaguchi, P. Rondon, and R. Jhala. Type-based data structure verification.
In PLDI, 2009.
18. V. Kuncak. Modular Data Structure Verification. PhD thesis, EECS Department,
Massachusetts Institute of Technology, February 2007.
19. S. Magill, J. Berdine, E. Clarke, and B. Cook. Arithmetic strengthening for shapeanalysis. In SAS, 2007.
20. S. Magill, M. Tsai, P. Lee, and Y. Tsay. Thor: A tool for reasoning about shapeand arithmetic. In CAV, 2008.
21. S. Magill, M. Tsai, P. Lee, and Y. Tsay. Automatic numeric abstractions for heapmanipulating programs. In POPL, 2010.
22. A. Møller and M. Schwartzbach. The pointer assertion logic engine. ACM SIGPLAN Notices, 36(5):221–231, 2001.
23. H. H. Nguyen, C. David, S. Qin, and W.-N. Chin. Automated verification of shapeand size properties via separation logic. In VMCAI, 2007.
24. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL — a proof assistant forhigher-order logic, volume 2283 of LNCS. Springer, 2002.
25. C. Popeea and W.-N. Chin. Inferring disjunctive postconditions. In Proceedingsof 11th Asian Computing Science Conference, 2006.
26. S. Qin, G. He, C. Luo, and W.-N. Chin. Loop invariant synthesis in a combined
domain. In ICFEM, 2010.
27. S. Qin, C. Luo, W.-N. Chin, and G. He. Automatically Refining Partial Specification for Program Verification. Technical Report, Teesside University, http://
www.scm.tees.ac.uk/s.qin/papers/refine.pdf, 2010.
28. J. Reynolds. Separation logic: a logic for shared mutable data structures. LICS02.
29. P. Rondon, M. Kawaguci, and R. Jhala. Liquid types. In PLDI, 2008.
30. M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic.
ACM Transactions on Programming Languages and Systems, 24(3):217–298, 2002.
31. S. Srivastava and S. Gulwani. Program verification using templates over predicate
abstraction. In PLDI, 2009.
32. H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. O’Hearn.
Scalable shape analysis for systems code. In CAV, 2008.