A Specialization Calculus for Pruning
Disjunctive Predicates to Support Verification
Wei-Ngan Chin1 Cristian Gherghina1 Răzvan Voicu1
Quang Loc Le1 Florin Craciun1 Shengchao Qin2
(1) Department of Computer Science, National University of Singapore(2) School of Computing, Teesside University

Abstract. Separation logic-based abstraction mechanisms, enhanced with userdefined inductive predicates, represent a powerful, expressive means of specifying heap-based data structures with strong invariant properties. However, expressive power comes at a cost: the manipulation of such logics typically requires theunfolding of disjunctive predicates which may lead to expensive proof search.
We address this problem by proposing a predicate specialization technique thatallows efficient symbolic pruning of infeasible disjuncts inside each predicate instance. Our technique is presented as a calculus whose derivations preserve thesatisfiability of formulas, while reducing the subsequent cost of their manipulation. Initial experimental results have confirmed significant speed gains from thedeployment of predicate specialization. While specialization is a familiar technique for code optimization, its use in program verification is new.

1 Introduction
Abstraction mechanisms are important for modelling and analyzing programs. Recent
developments allow richer classes of properties to be expressed via user-defined predicates for capturing commonly occurring patterns of program properties. Separation
logic-based abstraction mechanisms represent one such development. As an example,
the following predicate captures an abstraction of a sorted doubly-linked list.
data node { int val; node prev; node next; }dll(root, p, n, S) ≡ root=null ∧ n=0 ∧ S={}∨ ∃v, q, S1 · root7→node(v, p, q) ∗ dll(q, root, n−1, S1 )∧S = S1 ∪{v}∧∀a∈S1 · v≤ainv n≥0;
In this definition root denotes a pointer into the list, n the length of the list, S represents its set of values, whereas p denotes a backward pointer from the first node of the
doubly-linked list. The invariant n≥0 must hold for all instances of this predicate.
We clarify the following points. Firstly, spatial conjunction, denoted by the symbol ∗, provides a concise way of describing disjoint heap spaces. Secondly, this abstraction mechanism is inherently infinite, due to recursion in predicate definition. Thirdly,
a predicate definition is capable of capturing multiple features of the data structure it
models, such as its size and set of values. While this richer set of features can enhance
the precision of a program analysis, it inevitably leads to larger disjunctive formulas.

This paper is concerned with a novel way of handling disjunctive formulas, in conjunction with abstraction via user-defined predicates. While disjunctive forms are natural and expressive, they are major sources of redundancy and inefficiency. The goalof this paper is to ensure that disjunctive predicates can be efficiently supported in a
program analysis setting, in general, and program verification setting, in particular.
To achieve this, we propose a specialization calculus for disjunctive predicates that
supports symbolic pruning of infeasible states within each predicate instance. This allows for the implementation of both incremental pruning and memoization techniques.
As a methodology, predicate specialization is not a new concept, since general specialization techniques have been extensively used in the optimization of logic programs [18,17, 11]. The novelty of our approach stems from applying specialization to a new domain, namely program verification, with its focus on pruning infeasible disjuncts, rather
than a traditional focus on propagating static information into callee sites. This new useof specialization yields a fresh approach towards optimising program verification. Thisapproach has not been previously explored, since pervasive use of user-defined predicates in analysis and verification has only become popular recently (e.g. [14]). Our key
contributions are:
– We propose a new specialization calculus that leads to more effective program verification. Our calculus specializes proof obligations produced in the program verification process, and can be used as a preprocessing step before the obligations are
fed into third party theorem provers or decision procedures.
– We adapt memoization and incremental pruning techniques to obtain an optimized
version of the specialization calculus.
– We present a prototype implementation of our specialization calculus, integrated
into an existing program verification system. The use of our specializer yields significant reductions in verification times, especially for larger problems.
Section 2 illustrates the technique of specializing disjunctive predicates. Section 3
introduces the necessary terminology. Section 4 presents our calculus for specializing
disjunctive predicates and outlines its formal properties. Section 5 presents inference
mechanisms for predicate definitions to support our specialization calculus. Section 6presents experimental results which show multi-fold improvement to verification times
for larger problems. Section 7 discusses related work, prior to a short conclusion.

2 Motivating Example
Program states that are built from predicate abstractions are more concise, but may require properties that are hidden inside predicates. As an example, consider :dll(x, p1 , n, S1 ) ∗ dll(y, p2 , n, S2 ) ∧ x6=null
This formula expresses the property that the two doubly-linked lists pointed to by x
and y have the same length. Ideally, we should augment our formula with the property:
y6=null, n>0, S1 6={} and S2 6={}, currently hidden inside the two predicate instances but
may be needed by the program verification tasks at hand.
A naive approach would be to unfold the two predicate instances, but this would
blow up the number of disjuncts to four, as shown:

x=null ∧ y=null ∧ n=0 ∧ S1 ={} ∧ S2 ={} ∧ x6=null∨ y7→node(v2 , p2 , q2 ) ∗ dll(q2 , y, n−1, S4 ) ∧ x=null∧ S1 ={} ∧ n=0 ∧ S2 ={v2 } ∪ S4 ∧ n−1≥0 ∧ x6=null∨ x7→node(v1 , p1 , q1 ) ∗ dll(q1 , x, n−1, S3 ) ∧ y=null ∧ n=0∧ S1 ={v1 } ∪ S3 ∧ S2 ={} ∧ n−1≥0 ∧ x6=null∨ x7→node(v1 , p1 , q1 ) ∗ y7→node(v2 , p2 , q2 ) ∗ dll(q1 , x, n−1, S3 )∗ dll(q2 , y, n−1, S4 ) ∧ S1 ={v1 } ∪ S3 ∧ S2 ={v2 } ∪ S4 ∧ n−1≥0 ∧ x6=null
As contradictions occur in the first three disjuncts, we can simplify our formula to:x7→node(v1 , p1 , q1 ) ∗ y7→node(v2 , p2 , q2 ) ∗ dll(q1 , x, n−1, S3 )∗ dll(q2 , y, n−1, S4 ) ∧ S1 ={v1 } ∪ S3 ∧ S2 ={v2 } ∪ S4 ∧ n−1≥0 ∧ x6=null
After removing infeasible disjuncts, the propagated properties are exposed in the above
more specialized formula. However, this naive approach has the shortcoming that unfolding leads to an increase in the number of disjuncts handled, and its associated costs.
A better approach would be to avoid predicate unfolding, but instead apply predicate specialization to prune infeasible disjuncts and propagate hidden properties. Givena predicate pred(· · ·) that is defined by k disjuncts, we shall denote each of its specialized instances by pred(· · ·)@L, where L denotes a subset of the disjuncts, namelyL ⊆ {1. . . k}, that have not been pruned. Initially, we can convert each predicate instance pred(· · ·) to its most general form pred(· · ·)@{1. . . k}, while adding the basic
invariant of the predicate to its context. As an illustration, we may view the definitionof dll as a predicate with two disjuncts, labelled informally by 1: and 2: prior to eachof its disjuncts, as follows:dll(root, p, n, S) ≡ 1:(root=null ∧ n=0 ∧ S={})∨ 2:(root7→node(v, p, q) ∗ dll(q, root, n−1, S1 ) ∧ S = S1 ∪{v} ∧ ∀a∈S1 · v≤a)
We may convert each dll predicate by adding its invariant n≥0, as follows:
dll(x, p, n, S) =⇒ dll(x, p, n, S)@{1, 2} ∧ n≥0With our running example, this would lead to the following initial formula after thesame invariant n≥0 (from the two predicate instances) is added.
dll(x, p1 , n, S1 )@{1, 2} ∗ dll(y, p2 , n, S2 )@{1, 2}∧ x6=null ∧ n≥0This predicate may be further specialized with the help of its context by pruning away
disjuncts that are found to be infeasible. Each such pruning would allow more states tobe propagated by the specialized predicate. By using the context, x6=null, we can specialize the first predicate instance to dll(x, p1 , n, S1 )@{2} since this context contradicts
the first disjunct of the dll predicate. With this specialization, we may strengthen thecontext with a propagated state, namely n>0 ∧ S1 6={}, that is implied by its specialized
instance, as follows:
dll(x, p1 , n, S1 )@{2} ∗ dll(y, p2 , n, S2 )@{1, 2} ∧ x6=null ∧ n>0 ∧ S1 6={}Note that n≥0 is removed when a stronger constraint n>0 is added. The new constraint

pred ::= Wp(v ∗ ) ≡ Φ [inv π]Φ::=(∃w∗ ·σ)∗σ ::= κ∧πκ::= emp | v7→c(v ∗ ) | p(v ∗ ) | κ1 ∗ κ2π::= α | π1 ∧π2α::= β | ¬ββ::= v1 =v2 | v=null | a≤0 | a=0a::= k | k×v | a1 + a2 | max(a1 ,a2 ) | min(a1 ,a2 )where p is a predicate name; v, w are variable names;
c is a data type name; k is an integer constant;κ represents heap formulas; π represents pure formulas;
β represents atomic interpreted predicatesFig. 1. The Unannotated Specification Language.
n>0 now triggers a pruning of the second predicate instance, since its first disjunct canbe shown to be infeasible. This leads to a specialization of the second predicate, withmore propagation of atomic formulas, as follows:
dll(x, p1 , n, S1 )@{2} ∗ dll(y, p2 , n, S2 )@{2}∧ x6=null ∧ n>0 ∧ S1 6={} ∧ y6=null ∧ S2 6={}
In a nutshell, the goal of our approach is to apply aggressive specialization to our
predicate instances, without the need to resort to predicate unfolding, in the hope that
infeasible disjuncts are pruned, where possible. In the process, our specialization technique is expected to propagate states that are consequences of each of the specialized
predicate instances. We expect this proposal to support more efficient manipulation ofprogram states, whilst keeping the original abstractions intact where possible.

3 Formal Preliminaries
Our underlying computation model is a state machine with a countable set of variables
and a heap, which is a partial mapping from addresses to values.
Fig. 1 defines the syntax of our (unannotated) specification language. We denotesequences of variables v1 , . . . , vn by the notation v ∗ , and by β atomic interpreted predicates such as equality and disequality of program variables and arithmetic expressions.
Conjunctions of (possibly negated) atomic predicates form pure formulas, which wedenote by the symbol π. Heap formulas, denoted by κ, model the configuration of theheap. They rely on two important components: data constructors c(v ∗ ), which model
simple data records (e.g. the node of a tree), and inductively defined predicates, which
are generated by the non-terminal pred in Fig. 1.
Definition 1 (Heap Formula and Predicate Definition) A heap formula κ is either thesymbol emp, denoting the empty heap, or a formula of the form v7→c(v ∗ ), denoting asingleton heap, or a predicate p(v ∗ ), or finally, a formula of the form κ1 ∗ κ2 , where κ1and κ2 are heap formulas, and ∗ is the separating conjunction connective. Predicatesspred ::= p(v ∗ ) ≡ Φ̂; I; RWΦ̂::=(∃w∗ ·σ̂ | C)∗σ̂ ::= κ̂ ∧ πκ̂::= emp | v7→c(v ∗ ) | p(v ∗ )@L#R | κ̂1 ∗ κ̂2where p, v, w, c, π denote the same as in Fig. 1;
I is a family of invariants;
R is a set of pruning conditions.
C is a pure formula denoting a context computed in the specialization process.
Fig. 2. The Annotated Specification Language.

are defined inductively as the equivalence between a predicate symbol p(v ∗ ), and disjunctions of formulas of the form ∃w∗ · (κ ∧ π), where variables v ∗ may appear free.
Predicate definitions may be augmented with invariants specified by the inv keyword.
Unannotated formulas become annotated in the specialization process. Fig. 2 defines the syntax of the annotated specification language. Annotated predicate definitions
are generated by the nonterminal spred.
Definition
Given a predicate definition
W 2 (Annotated Predicates and Formulas)p(v ∗ ) ≡ W (∃w∗ ·κ∧π)∗ , the corresponding annotated predicate definition has the formp(v ∗ ) ≡(∃w∗ ·κ̂ ∧ π | C)∗ ; I; R, where I is a family of invariants, and R is a set ofpruning conditions. Each disjunct ∃w∗ ·κ̂ ∧ π | C now contains the annotated counterpartκ̂ of κ, and is augmented with a context C, which is a pure formula for which C → π
always holds. Intuitively, C captures also the consequences of the specialized states of κ̂.
An annotated formula is a formula where all the predicate instances are annotated. An
annotated predicate instance is of the form p(v ∗ )@L#R, where L⊆{1, .., n} is a set oflabels denoting the unpruned disjuncts, and where R ⊆ R is a set of remaining pruning
conditions. The set of invariants I is of the form {(L→πL ) | ∅⊂L⊆{1, .., n}}. For each setof labels L, πL represents the invariant for the specialized predicate instance p(v ∗ )@L.
For a given annotated predicate instance p(v ∗ )@L#R, it is possible for L = ∅. When
this occurs, it denotes that none of the predicate’s disjuncts are satisfiable. Moreover,
we have π∅ =f alse which will contribute towards a false state (or contradiction) for its
given context.
Definition 3 (Pruning Condition)
The set of pruning conditions R is of the form{(α←L) | · · · }. A pruning condition is a pair between an atomic predicate instance α
and a set of labels L, written α←L. Its intuitive meaning is that the disjuncts in L should
be kept if α is satisfiable in the current context.
Wn
Given a predicate definition p(v ∗ ) ≡ i=1 (∃w∗ ·σ̂i | Ci ); I; R, we call Di =df(∃w∗ ·σ̂i | Ci ) the ith disjunct of p ; i will be called the label of its disjunct. We shalluse Di freely as the ith disjunct of the predicate at hand whenever there is no risk ofconfusion. We employ a notion of closure for a given conjunctive formula. Consider aformula π(w∗ ) = ∃v ∗ ·α1 ∧· · ·∧αm , where αi are atomic predicates, and variables w∗
appear free. We denote by S = closure(π(w∗ )) a set of atomic predicates (over the freevariables w∗ ) such that each element α ∈ S is entailed by π(w∗ ). Some of the variablesw∗ may appear free in α but not v ∗ . To ensure this closure set be finite, we also impose arequirement that weaker atomic constraints are never present in the same set, as follows:∀αi ∈ S · ¬(∃αj ∈ S · i6=j ∧ αi =⇒ αj ). Ideally, closure(π(w∗ )) contains all stronger
atomic formulas entailed by π(w∗ ), though depending on the abstract domain used, thisset may not be computable. A larger closure set leads to more aggressive pruning.
Our specialization calculus (Sec 4) is based on the annotated specification language.
We have an initialization and inference process (Sec 5) to automatically generate allannotations (including I, R) that are required by specialization. For simplicity of presentation, we only include normalized linear arithmetic constraints in our language. Our
system currently supports both arbitrary linear arithmetic constraints, as well as set constraints. This is made possible by integrating the Omega [19] and MONA solvers [9]into the system. In principle, the system may support arbitrary constraint domains, provided that a suitable solver is available for the domain of interest. Such a solver should
be capable of handling conjunctions efficiently, as well as computing approximationsof constraints that convert disjunctions into conjunctions (e.g. hulling).

4 A Specialization Calculus
Our specialization framework detects infeasible disjuncts in predicate definitions without explicitly unfolding them, and computes a corresponding strengthening of the purepart while preserving satisfiability. We present this as a calculus consisting of specialization rules that can be applied exhaustively to convert a non-specialized annotatedformula1 into a fully specialized one, with stronger pure parts, that can be subsequently
extracted and passed on to a theorem prover for satisfiability/entailment checking. Apartfrom being syntactically correct, annotated formulas must satisfy the following wellformedness conditions.
Definition 4 (Well-formedness) For each annotated predicate p(v∗ )@L#R in the forW
mula at hand, assuming the definition p(v ∗ )≡ ni=1 Di ; I; R, we have that (a) L ⊆{1, . . . , n} ; (b) R ⊆ R ; and (c) forall α←L0 ∈ R we have L ∩ L0 6= ∅.
Definition 5 (Specialization Step)A
specialization step has the form
Φ̂1 | C1 −sf→ Φ̂2 | C2 , and denotes the relation allows the annotated formula Φ̂1 with
context C1 to be transformed into a more specialized formula Φ̂2 with context C2 .
Our calculus produces specialization steps, which are applied in sequence, exhaustively, to produce fully specialized formulas (a formal definition of such formulas will
be given below). Relation −sf→ depends on relation −sp→, which produces predicate
specialization steps defined by the following:
Definition 6 (Predicate Specialization Step) A predicate specialization step has form(1)p(v ∗ )@L1 #R1 | C1 −sp→ p(v ∗ )@L2 #R2 | C2 .

and signifies that annotated predicate p(v ∗ )@L1 #R1 | C1 can be specialized intop(v ∗ )@L2 #R2 | C2 , where L2 ⊆ L1 , R2 ⊂ R1 , and C2 is stronger than C1 .
1

The conversion of non-annotated formulas into annotated ones shall be presented in Sec. 5.

[SP−[FILTER]]
Rf = {(α←L0 ) | (α←L0 )∈R, (L∩L0 =∅)∨(C =⇒ α)}
C, L ⊢ R −filter→ (R − Rf )[SP−[PRUNE]]C∧α =⇒ false (α←L0 ) ∈ R L ∩ L0 6= ∅ L2 = L − L0
C1 = Inv(p(v ∗ ), L2 )C ∧ C1 , L2 ⊢ R −filter→ R1
p(v ∗ )@L#R | C −sp→ p(v ∗ )@L2 #R1 | C ∧ C1
[SP−[FINISH]]
C, L ⊢ R −filter→ ∅R 6= ∅p(v ∗ )@L#R | C −sp→ p(v ∗ )@L#∅ | C
Fig. 3. Single-step Predicate Specialization

Here, the sets L1 and L2 denote sets of disjuncts of p(v ∗ ) that have not been detected
to be infeasible. Each specialization step aims at detecting new infeasible disjuncts andremoving them during the transformation. Thus L2 is expected to be a subset of L1 .
The sets of pruning conditions R1 and R2 may be redundant, but are instrumental
in making specialization efficient. They record incremental changes to the state of thespecializer, and represent information that would be expensive to re-compute at every
step. Essentially, a pruning condition α←L0 states that whenever ¬α is entailed by thecurrent context, the disjuncts whose labels are in L0 can be pruned. The initial set ofpruning conditions is derived when converting formulas into annotated formulas, and isformally discussed in Section 5.
In a nutshell, each specialization step of the form (1) detects (if possible) a pruning condition α←L0 ∈ R such that if ¬α is entailed by the current context, then the
disjuncts whose labels occur in L0 are infeasible and can be pruned. Given the notations in (1), this is achieved by setting L2 = L1 − L0 . Subsequently, the current set ofpruning conditions is reduced to contain only elements of the form α′ ←L′0 such thatL′0 ∩ L2 6= ∅. Thus, the well-formedness of the annotated formula is preserved
A key aspect of specialization is that context strengthening helps reveal and prune
mutually infeasible disjuncts in groups of predicates, which leads to a more aggressive
optimization as compared to the case where predicates are specialized in isolation.
Definition 7 (Fully Specialized Formula; Complete Specialization) An annotatedformula is fully specialized w.r.t a context when all its annotated predicates have empty
pruning condition sets. If the initial pruning condition sets are computed using a notionof strongest closure, then for each predicate in the fully specialized formula, all theremaining labels in the predicate’s label set denote feasible disjuncts with respect tothe current context, and in that sense, the specialization is complete.
This procedure is formalized in the calculus rules given in Figures 3 and 4. Figure 3 defines the predicate specialization relation −sp→. This relation has two main
components: the one represented by the rule [SP−[FILTER]], which restores the wellformedness of an annotated predicate, and the one represented by the rule [SP−[PRUNE]],
which detects infeasible disjuncts and removes the corresponding labels from the annotation. A third rule, [SP−[FINISH]] produces the fully specialized predicate.

[SF−[PRUNE]]p(v ∗ )@L#R | C −sp→ p(v ∗ )@L2 #R2 | C2
p(v ∗ )@L#R ∗ κ̂ | C −sf→ p(v ∗ )@L2 #R2 ∗ κ̂ | C2
[SF−[CASE−SPLIT]]⊢ C =⇒ α1 ∨α2 ⊢ α1 ∧α2 =⇒ false∀i ∈ {1, 2} · κ̂ | C∧αi −sf→ κ̂i | Ci
κ̂ | C −sf→ (κ̂1 | C1 ) ∨ (κ̂2 | C2 )[SF−[OR]]κ̂1 | C1 −sf→ κ̂3 | C3
(κ̂1 | C1 ) ∨ (κ̂2 | C2 ) −sf→ (κ̂3 | C3 ) ∨ (κ̂2 | C2 )Fig. 4. Single-step Formula Specialization

The predicate specialization relation can be weaved into the formula specialization
relation given in Fig. 4. The first rule, [SF−[PRUNE]], defines the part of the −sf→ relation which picks a predicate in a formula and transforms it using the −sp→ relation,leaving the rest of the predicates unchanged. However, the transformation of the predicate’s context is incorporated into the transformation of the formula’s context. This
rule realizes the potential for cross-specialization of predicates, eliminating disjuncts ofdifferent predicates that are mutually unsatisfiable.
The rule [SF−[CASE−SPLIT]] allows further specialization via case analysis. It defines the part of the −sf→ relation that produces two instances of the same formula,joined in a disjunction, each of the new formulas having a stronger context. Eachstronger context is produced by conjunction with an atom αi , i ∈ {1, 2}, with the requirement that the two atoms be disjoint and their disjunction cover the original context
C. This rule is instrumental in guaranteeing that all predicates reach a fully specialized
status. Indeed, whenever an annotated predicate has a pruning condition α←L0 , suchthat α is not entailed by the context C, yet α ∧ C is satisfiable, the only way to further
specialize the predicate is by case analysis with the atoms α and ¬α. Finally, the rule
[SF−[OR]] handles formulas with multiple disjunctions.
In the remainder of this section, we formalize the notion that our calculus produces
terminating derivations, and is sound and complete.
Property 1 Relations −sp→ and −sf→ preserve well-formedness. Thus, given two annotated predicate instances p(v∗ )@L1 #R1 and p(v∗ )@L2 #R2 , ifp(v∗ )@L1 #R1 | C1 −sp→ p(v∗ )@L2 #R2 | C2

can be derived from the calculus, and p(v∗ )@L1 #R1 is well-formed, then p(v∗ )@L2 #R2
is well-formed as well. Moreover, for all annotated formulas Φ̂1 and Φ̂2 , ifΦ̂1 | C1 −sf→ Φ̂2 | C2

can be derived from the calculus, and Φ̂1 is well-formed, then Φ̂2 is well formed as well.
A predicate specialization sequence is a sequence of annotated predicates such thateach pair of consecutive predicates is in the relation −sp→. A formula specialization se-quence is a sequence of annotated formulas such that each pair of consecutive formulas
is in the −sf→ relation.
Definition 8 (Canonical Specialization Sequence) A canonical specialization sequenceis a formula specialization sequence where (a) the first element is well-formed; (b) specialization rules are applied exhaustively ; (c) the [SF−[CASE−SPLIT]] relation is only
applied as a last resort (i.e. when no other relation is applicable); and (d) the caseanalysis atoms for the [SF−[CASE−SPLIT]] relation must be of the form α, ¬α, whereα←L0 is a pruning condition occurring in an annotated predicate p(v∗ )@L#R of theformula, such that L ∩ L0 6= ∅.
Property 2 (Termination) All canonical specialization sequences are finite and produce either fully specialized formulas, or formulas whose context is unsatisfiable.
Property 3 (Soundness) The −sp→ and −sf→ relations preserve satisfiability. Thus,
if p(v0..n )@L1 #R1 | C1 −sp→ p(v0..n )@L2 #R2 | C2 can be derived from the calculus,
then for all heaps h and stacks s, s, h |= p(v∗ )@L1 #R1 | C1 iff s, h |=p(v∗ )@L2 #R2 | C2 . Moreover, if Φ̂1 | C1 −sf→ Φ̂2 | C2 can be derived from the calculus,
then s, h |= Φ̂1 |C1 iff s, h |= Φ̂2 |C2 .
We note here that the set R does not play a role in the way an annotated predicate
is interpreted. Mishandling R (as long as no elements are added) may result in lack oftermination or incompleteness, but does not affect soundness.
Finally, we address the issue of completeness. This property, however, is dependent on how “complete” the conversion of a predicate into its annotated form is. Thus,
we shall first give an ideal characterization of such a conversion, after which we shallendeavour to prove the completeness property. Realistic implementations of this conversion shall be discussed in Section 5.
Definition 9 (Strongest Closure) The strongest closure of unannotated formula Φ, denoted sclosure(Φ), is the largest set of atoms α with the following properties: (a) for all
stacks s, s |= α whenever there exists h such that s, h |= Φ, and (b) if α is not of theform v6=null, then there exists no atom α′ strictly stronger than α – that is, it is not thecase that for all s, s |= α whenever s |= α′ . For practical and termination reasons, weshall assume only closures which return finite sets in our formulation.
In our conversion of an unannotated predicate definition for p(v ∗ ) into the annotatedW
definition p(v ∗ )≡ ni=1 Di ; I; R, we compute the following sets: Gi = sclosure(Di ∧π),′′for i = 1, .., n, HL = {α | forall i ∈ L, exists
V α ∈ Gi s.t. forall s, s |= α whenever s |=α} and T
I = {L→π | L⊆{1...n}, π = α∈HL α}, and R = {α←L | L is the largest set
s.t. α∈ i∈L Gi }. Moreover, we introduce the notation Inv(p(v ∗ ), L) = πL , where(L→πL )∈I. This notation is necessary in applying the rule [SP−[PRUNE]].
In practice, either the assumption holds, or the closure procedure computes a closeenough approximation to the strongest closure so that very few, if any, infeasible disjuncts are left in the specialized formula.
Property 4 (Completeness) Let p(v∗ )@L#∅ ∗ σ̂|C be a fully specialized formula that
resulted from a specialization process that started with an annotated formula. Denoteby πi , 1 ≤ i ≤ n the pure parts of the disjuncts in the definition of p(v∗ ), and assume
that C is satisfiable. Then, for all i ∈ L, πi ∧ C is satisfiable.
Proofs of the above properties, as well as a more detailed discussion of our calculus
rules, can be found in [3].

5 Inferring Specializable Predicates
We present inference techniques that must be applied to each predicate definition so thatthey can support the specialization process. We refer to this process as inference for specializable predicates. A predicate is said to be specializable if it has multiple disjuncts
and it has a non-empty set of pruning conditions. These two conditions would allow a
predicate instance to be specializable from one form to another specialized form. Our
predicates are processed in a bottoms-up order with the following key steps:– Transform each predicate definition to its specialized form.
– Compute an invariant (in conjunctive form) for each predicate.
– Compute a family of invariants to support all specialized instances of the predicate.
– Compute a set of pruning conditions for the predicate.
– Specialize recursive invocations of the predicate, if possible.
As a running example for this inference process, let us consider the following predicate which could be used to denote a list segment of singly-linked nodes:
data snode { int val; snode next; }lseg(x, p, n) ≡ x=p ∧ n=0 ∨ ∃q, m · x7→snode( , q) ∗ lseg(q, p, m) ∧ m=n−1
Our inference technique derives the following specializable predicate definition:lseg(x, p, n) ≡ x=p ∧ n=0 | x=p∧n=0 ∨∃q, m · x7→snode( , q)∗lseg(q, p, m)∧m=n−1 | x6=null∧n>0;
I = {{1}→x=p∧n=0, {2}→x6=null∧n>0, {1, 2}→n≥0};
R = {x=p←{1}, n=0←{1}, x6=null←{2}, n>0←{2}}
Note that we have a family of invariants, named I , to cater to each of the specializedstates. The most general invariant for the predicate is Inv(lseg(x, p, n), {1, 2}) = n≥0.
This is computed by a fix-point analysis [4] on the body of the predicate. If we determine that a particular predicate instance can be specialized to lseg(x, p, n)@{2}, we
may use a stronger invariant Inv(lseg(x, p, n), {2}) = x6=null ∧ n>0 to propagate thisconstraint from the specialized instance. Such a family of invariants allows us to enrich
the context of the predicate instances that are being progressively specialized.
Furthermore, we must process the predicate definitions in a bottom-up order, sothat predicates lower in the definition hierarchy are inferred before predicates higher inthe hierarchy. This is needed since we intend to specialize the body of each predicate
definition with the help of specialized definitions that were inferred earlier. In the caseof a set of mutually-recursive predicate definitions, we shall process this set of predicates simultaneously. Initially, we shall assume that the set of pruning conditions foreach recursive predicate is empty, which makes its recursive instances unspecializable.
However, once its set of pruning conditions has been determined, we can apply further
specialization so that the recursive invocations of the predicate are specialized as well.
The formal rules for inferring each specializable predicate are given in Fig. 5. The
rule [INIT−[MULTI−SPEC]] converts an unannotated formula into its corresponding specialized form. It achieves this by an initialization step via the −if→ relation given in
Fig. 6, followed by a multi-step specialization using −sf→∗ , without resorting to casespecialization (that would otherwise result in an outer disjunctive formula). This essentially applies a transitive closure of −sf→ until no further reduction is possible.

[INIT−[MUTLI−SPEC]]κ∧π −if→ κ̂∧π | C1
κ̂ | C1 −sf→∗ κ̂1 | C2κ∧π −msf→ κ̂1 ∧π | C2
[ISP−[SPEC−BODY]]
W∗
spredold = (p(v∗ ) ≡ n∀i∈{1, .., n} · σi −msf→ σ̂i | Ci
i=1 (∃ui · σi ))Wn∗sprednew = (p(v ) ≡ i=1 (∃u∗i · σ̂i | Ci ))spredold −isp→ sprednew[ISP−[BUILD−INV−FAMILY] ]W
W∗∗
spredold = (p(v∗ ) ≡ n
ρ = [invp (v∗ )7→fix( ni=1 (∃ui · σ̂i | Ci ))i=1 ∃ui · Ci )]W∗∗
I = {(L→hull( i∈L ∃ui · ρCi ) | ∅⊂L⊂{1..n}} ∪ {{1..n}→ρ(invp (v ))}W∗
sprednew = (p(v∗ ) ≡ n
i=1 (∃ui · σ̂i | ρCi ); I)
spredold −isp→ sprednew[ISP−[BUILD−PRUNE−COND]]
Wn
S
spredold = (p(v ) ≡ i=1 (∃u∗i · σ̂i | Ci ); I)
G= ni=1 closure(I({i}))SR = α∈G {α←{i | 1≤i≤n ∧ I({i}) =⇒ α}} ∀i∈{1, .., n} · σ̂i | Ci −sf→∗ σ̂i,2 | Ci,2W∗
sprednew = (p(v∗ ) ≡ n
i=1 (∃ui · σ̂i,2 | Ci,2 ); I; R)∗

spredold −isp→ sprednew∗

where −sf→ is the transitive closure of −sf→; and I({i}) = πi , given ({i}→πi ) ∈ I.
Fig. 5. Inference Rules for Specializable Predicates

The rule [ISP−[SPEC−BODY]] converts the body of each predicate definition into
its specialized form. For each recursive invocation, it will initially assume a symbolic
invariant, named invp (v∗ ), without providing any pruning conditions. This immediately
puts each recursive predicate instance in the fully-specialized form.
After the body of the predicate definition has been specialized, we can proceed tobuild a constraint abstraction for its predicate’s invariant, denoted by invp (v∗ ), in the[ISP−[BUILD−INV−FAMILY] ] rule. For example, we may denote the invariant of predicate lseg(x, p, n) symbolically using invlseg (x, p, n), before building the following recursive constraint abstraction:
invlseg (x, p, n) ≡ x=p∧n=0 ∨ ∃q, m · x6=null∧n=m+1∧invlseg (q, p, m)

If we apply a classical fix-point analysis to the above abstraction, we would obtain aclosed-form formula as the invariant of the lseg predicate, that is invlseg (x, p, n) = n≥0.
With this predicate invariant, we can now build a family of invariants for each proper
subset L of disjuncts, namely 0⊂L⊂{1..n}. This is done with the help of the convex hull
approximation. The size of this family of invariants is exponential to the number of
disjuncts. While this is not a problem for predicates with a small number of disjuncts,
it could pose a problem for unusual predicates with a large number of disjuncts. To
circumvent this problem, we could employ either a lazy construction technique or amore aggressive approximation to cut down on the number of invariants generated. For
simplicity, this aspect is not considered in the present paper.

[INIT−[EMP]]
emp −ih→ emp | true

[INIT−[CELL]]x7→p(v ∗ ) −ih→ x7→p(v ∗ ) | x6=null[INIT−[PRED]]W∗p(v ∗ ) ≡ ( ni=1 (∃ui ·σ̂i | Ci )); I; R
C = Inv(p(v ∗ ), {1..n})∗p(v ) −ih→ p(v ∗ )@{1..n}#R | C[INV−DEF]

p(v ∗ ) ≡ (Wn∗
i=1 (∃ui ·σ̂i | Ci )); I; R

(L→C) ∈ I
Inv(p(v ∗ ), L) = C[INIT−[HEAP]]∀i∈{1, 2}·κi −ih→ κ̂i | Ci

[INIT−[FORMULA]]κ −ih→ κ̂ | C

κ1 ∗κ2 −ih→ κ̂1 ∗κ̂2 | C1 ∧C2κ∧π −if→ κ̂∧π | C∧π

Fig. 6. Initialization for Specialization

Our last step is to build a set of pruning conditions for the disjunctive predicatesusing the [ISP−[BUILD−PRUNE−COND]] rule. This is currently achieved by applying aclosure operation over the invariant I({i}) for each of the disjuncts. To obtain a more
complete set of pruning conditions, we are expected to generate a set of strong atomic
constraints for each of the closure operations. For example, if we currently have a formula a>b ∧ b>c, a strong closure operation over this formula may yield the following
set of atomic constraints {a>b, b>c, a>c+1} as pruning conditions and omit weakeratomic constraints, such as a>c.
Definition 10 (Sound invariant and sound pruning condition) Given a predicate defW
inition p(v ∗ )≡ ni=1 Di ; · · · :(1) an invariant L→π is said to be sound w.r.t. the predicate p if (1.a) ∅ ⊂ L ⊆ {1, .., n},and (1.b) p(v ∗ )@L# |= π.
(2) a family of invariants I is sound if every invariant from I is sound and the domainof I is the set of all non-empty subsets of {1, .., n};(3) a pruning condition (α←L) is sound w.r.t. the predicate p if (3.a) ∅ ⊂ L ⊆ {1, .., n},(3.b) vars(α) ⊆ {v ∗ }, and (3.c) ∀i∈L·Di |= α.
(4) a set of pruning conditions R is sound if every pruning condition in R is sound w.r.t.
the predicate p.
Property 5 For each predicate p(v ∗ ), the family of invariants and the set of pruning
conditions derived for p by our inference process are sound, assuming the fixpoint analysis and the hulling operation used by the inference are sound.
A proof of this property can be found in [3].

6 Experiments
We have built a prototype system for our specialization calculus inside an existing program verification system for separation logic, called HIP [14]. Our implementation
benefits greatly from two optimizations: memoization and incremental pruning. The
key here is to support the early elimination of infeasible states, by attempting a proof

Programs (specified props) LOC
17 small progs (size)
87
Bubble sort (size,sets)
80
Quick sort (size,sets)
115
Merge sort (size,sets)
128
Complete (size,minheight) 137
AVL (height, size,bal)
160
Heap Trees (size, maxelem) 208
AVL (height, size)340
AVL (height, size, sets) 500
Red Black (size, height) 630

HIP HIP+Spec
HIP
HIP+Spec
Time(s) Time(s) Count Disj Size Count Disj Size
0.86
0.80
229 1.63 12.39 612 1.13 2.97
2.20
2.23
296 2.13 18.18 876 1.09 2.79
2.43
2.13
255 3.29 17.97 771 1.27 3.08
3.10
2.15
286 2.04 16.74 1079 1.07 2.99
5.01
2.94
463 3.52 43.75 2134 1.11 10.10
64.1
16.4
764 2.90 85.02 6451 1.07 9.66
14.9
4.62
649 2.10 56.46 2392 1.02 8.68
27.5
13.1
704 2.98 70.65 7078 1.09 10.74
657
60.7
1758 8.00 86.79 14662 1.91 10.11
25.2
15.6
2225 3.84 80.91 7697 1.01 3.79

Fig. 7. Verification Times and Proof Statistics (Proof Counts, Avg Disjuncts, Avg Size)of each atomic constraint α being in contradiction with a given context C. In this way,
the context C is allowed to evolve to a monotonically stronger context C1 , such that
C1 =⇒ C. Hence, if indeed C =⇒ ¬α is established, we can be assured that C1 =⇒ ¬αwill also hold. This monotonic context change is the basis of the memoization optimization that leads to reuse of previous outcomes of implications and contradictions.
More specifically, we maintain a memoization set, I, for each context C. This denotes a set of atomic constraints that are implied by the context C; that is ∀α∈I· C =⇒ α.
Contradictions of the form (C∧α) = false are also memoized in the same way, since we
can model it as an implication check C =⇒ ¬α. These memoization recalls are only
sound approximations of the corresponding implication checks. In case both membership tests fail for a given pruning condition α, we could turn to automated provers (as alast resort) to help determine C =⇒ ¬α. Memoization would, in general, help minimize
on the number of invocations to the more costly provers.
The early elimination of infeasible states has an additional advantage. We can easily
slice out relevant constraints from a (satisfiable) context C that is needed to prove an
atomic constraint α. This is possible because we detect infeasible branches by proving only one atomic pruning constraint at a time. For example, consider a context
x6=null ∧ n>0 ∧ S6={}. If we need to prove its contradiction with n=0, a naive solution is to use (x6=null ∧ n>0 ∧ S6={}) =⇒ ¬(n=0). A better solution is to slice out justthe constraint n>0, and then proceed to prove the contradiction using n>0 =⇒ ¬(n=0),
leading to an incremental pruning approach that uses smaller proof obligations. To implement this optimization, we partition each context into sets of connected constraints.
Two atomic constraints in a context C are said to be connected if they satisfy the following relation.
connected(α1 , α2 ) :- (vars(α1 )∩vars(α2 )) 6= {}connected(α1 , α2 ) :- ∃α∈C · connected(α1 , α)∧connected(α2 , α)Using this relation, we can easily slice out a set of constraints (from the context) thatare connected to each pruning condition.
Fig 7 summarizes a suite of programs tested which included the 17 small programs (comprised of various methods on singly, doubly, sorted and circular linked lists,
selection-sort, insertion-sort and methods for handling heaps, and perfect trees). Due
to similar outcomes, we present the average of the performances for these 17 programs.

HIP %
100

75

HIP + Spec :Avg.
Disjuncts

50

Avg. Size
25Time
0
17 smallprogs

Bubble
sort

Quick
sort

Merge Complete AVL
sort(h, s,b)

Heap
Trees

AVL
(h, s)AVL(h, s, s)

Red
Black

Fig. 8. Characteristic (disjunct, size, timing) of HIP+Spec compared to the Original HIP

We also experimented with a set of medium-sized programs that included complex
shapes and invariants, to support full functional correctness. We measured the verification times taken for the original HIP system, and also the enhanced system, called
HIP+Spec, with predicate specialization. For the suite of simple programs, the verifier with specializer runs about 7% faster. For programs with more complex properties(with the exception of bubble sort), predicate specialization manages to reduce verification times by between 12% and 90%. These improvements were largely due to thepresence of smaller formulae with fewer disjuncts, as captured in Fig 8. This graphcompares the characteristics (e.g. average disjuncts, sizes and timings) of formula encountered by HIP+Spec, as a percentage relative to the same properties of the original
HIP system. For example, the average number of disjuncts per proof encountered went
down from 3.2 to 1.1; while the size of each proof (based on as the number of atomic
formulae) also decreased from an average of 48.0 to 6.5. This speed-up was achieved
despite a six fold increase in the proof counts per program from 763 to 4375 used by
the specialization and verification processes. We managed to achieve this improvement
despite the overheads of a memoization mechanism and the time taken to infer annotations for specializable predicates. We believe this is due to smaller and simpler proof
obligations generated with the help our specialization process.
We also investigated the effects of various optimizations on the specialization mechanism. Memoizing implications and contradictions saves 3.47%, while memoizing eachcontext for state change saves 22.3%. For incremental pruning, we have utilized the slicing mechanism which saves 48% on average. We have not yet exploited the incremental
proving capability based on strengthening of contexts since our current solvers, Omega
and MONA, do not support such a feature. These optimizations were measured separately, with no attempt made to study their correlation. For an extended version of thepresent paper, including further experimental details, cf. [3].

7 Related Work and Conclusion
Traditionally, specialization techniques [8, 17, 11] have been used for code optimization by exploiting information about the context in which the program is executed.

Classical examples are the partial evaluators based on binding-time analysers that divide a program into static parts to be specialized and dynamic parts to be residualized.
However, our work focusses on a different usage domain, proposing a predicate specialization for program verification to prune infeasible disjuncts from abstract program
states. In contrast, partial evaluators [8] use unfolding and specialised methods to propagate static information. More advanced partial evaluation techniques which integrate
abstract interpretation have been proposed in the context of logic and constraint logic
programming [18, 17, 11]. They can control the unfolding of predicates by enhancing
the abstract domains with information obtained from other unfolding operations. Our
work differs in its focus on minimizing the number of infeasible states, rather than oncode optimization. This difference allows us to use techniques, such as memoizationand incremental pruning, that were not previously exploited for specialization.
SAT solvers usually use a conflict analysis [22] that records the causes of conflicts
so as to recognize and preempt the occurrences of similar conflicts later on in the search.
Modern SMT solvers (e.g. [15, 6]) use analogous analyses to reduce the number of calls
to underlying theory solvers. Compared to our pruning approach, conflict analysis [22]is a backtracking search technique that discovers contexts leading to conflicts and uses
them to prune the search space. These techniques are mostly complementary since they
did not consider predicate specialization, which is important for expressive logics.
The primary goal of our work is to provide a more effective way to handle disjunctive predicates for separation logic [14, 13]. The proper treatment of disjunction (toachieve a trade-off between precision and efficiency) is a key concern of existing shapeanalyses based on separation logic [5, 10]. One research direction is to design parameterized heap materialization mechanisms (also known as focus operation) adapted to
specific program statements and to specific verification tasks [21, 12, 20, 1, 16]. Anotherdirection is to design partially disjunctive abstract domains with join operators that enable the analysis to abstract away information considered to be irrelevant for proving
a certain property [7, 23, 2]. Techniques proposed in these directions are currently orthogonal to the contribution of our paper and it would be interesting to investigate if
they could benefit from predicate specialization, and vice-versa.
Conclusion. We have proposed in this paper a specialization calculus for disjunctive
predicates in a separation logic-based abstract domain. Our specialization calculus isproven sound and is terminating. It supports symbolic pruning of infeasible states withineach predicate instance, under monotonic changes to the program context. We havedesigned inference techniques that can automatically derive all annotations required foreach specializable predicate. Initial experiments have confirmed speed gains from thedeployment of our specialization mechanism to handle separation logic specificationsin program verification. Nevertheless, our calculus is more general, and is useful for
program reasoning over any abstract domain that supports disjunctive predicates. This
modular approach to verification is being enabled by predicate specialization.
Acknowledgement We thank the reviewers for insightful feedback. This work is being
supported principally by MoE research grant R-252-000-411-112.

References
1. J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O’Hearn, T. Wies, and H. Yang. Shapeanalysis for composite data structures. In CAV, pages 178–192, 2007.

2. B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. In POPL, pages 247–260,
2008.
3. W.N. Chin, C. Gherghina, R. Voicu, Q.L. Le, F. Craciun, and Qin S.C.
A
specialization calculus for pruning disjunctive predicates to support verification.
Technical report, School of Computing, National University of Singapore, 2011,
http://loris-7.ddns.comp.nus.edu.sg/ e project/hippruning/.
4. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis
of programs by construction or approximation of fixpoints. In ACM POPL, pages 238–252,
1977.
5. D. Distefano, P. W. O’Hearn, and H. Yang. A local shape analysis based on separation logic.
In TACAS, pages 287–302, 2006.
6. B. Dutertre and L. M. de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In CAV,
pages 81–94, 2006.
7. B. Guo, N. Vachharajani, and D. I. August. Shape analysis with inductive recursion synthesis.
In ACM PLDI, pages 256–265, 2007.
8. N.D. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.
9. N. Klarlund and A. Moller. MONA Version 1.4 - User Manual. BRICS Notes Series, January
2001.
10. V. Laviron, B.-Y. Evan Chang, and X. Rival. Separating shape graphs. In ESOP, pages
387–406, 2010.
11. M. Leuschel. A framework for the integration of partial evaluation and abstract interpretationof logic programs. ACM Trans. Program. Lang. Syst., 26(3):413–463, 2004.
12. R. Manevich, J. Berdine, B. Cook, G. Ramalingam, and M. Sagiv. Shape analysis by graphdecomposition. In TACAS, pages 3–18, 2007.
13. H. H. Nguyen and W.-N. Chin. Enhancing program verification with lemmas. In CAV, pages
355–369, 2008.
14. H.H. Nguyen, C. David, S.C. Qin, and W.N. Chin. Automated Verification of Shape And
Size Properties via Separation Logic. In VMCAI, pages 251–266, January 2007.
15. R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Solving SAT and SAT Modulo Theories: Froman abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM, 53(6):937–
977, 2006.
16. A. Podelski and T. Wies. Counterexample-guided focus. In ACM POPL, pages 249–260,
2010.
17. G. Puebla and M. Hermenegildo. Abstract specialization and its applications. In ACM
SIGPLAN PEPM, pages 29–43, 2003.
18. G. Puebla, M. Hermenegildo, and J. P. Gallagher. An integration of partial evaluation in a
generic abstract interpretation framework. In ACM SIGPLAN PEPM, pages 75–84, January
1999.
19. W. Pugh. The Omega Test: A fast practical integer programming algorithm for dependence
analysis. Communications of the ACM, 8:102–114, 1992.
20. N. Rinetzky, A. Poetzsch-Heffter, G. Ramalingam, M. Sagiv, and E. Yahav. Modular shapeanalysis for dynamically encapsulated programs. In ESOP, pages 220–236, 2007.
21. M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM
Trans. Program. Lang. Syst., 24(3):217–298, 2002.
22. J. P. Marques Silva and K. A. Sakallah. GRASP—a new search algorithm for satisfiability.
In International Conference on Computer-Aided Design, pages 220–227, 1996.
23. H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. W. O’Hearn. Scalable shape analysis for systems code. In CAV, pages 385–398, 2008.