9

arXiv:1710.09635v3 [cs.LO] 8 Nov 2017

Automated Lemma Synthesis in Symbolic-Heap
Separation Logic
QUANG-TRUNG TA∗ , School of Computing, National University of Singapore, Singapore
TON CHANH LE, School of Computing, National University of Singapore, Singapore
SIAU-CHENG KHOO, School of Computing, National University of Singapore, Singapore
WEI-NGAN CHIN, School of Computing, National University of Singapore, Singapore
The symbolic-heap fragment of separation logic has been actively developed and advocated for verifying the
memory-safety property of computer programs. At present, one of its biggest challenges is to effectively prove
entailments containing inductive heap predicates. These entailments are usually proof obligations generated
when verifying programs that manipulate complex data structures like linked lists, trees, or graphs.
To assist in proving such entailments, this paper introduces a lemma synthesis framework, which automatically
discovers lemmas to serve as eureka steps in the proofs. Mathematical induction and template-based constraint
solving are two pillars of our framework. To derive the supporting lemmas for a given entailment, the
framework firstly identifies possible lemma templates from the entailment’s heap structure. It then sets
up unknown relations among each template’s variables and conducts structural induction proof to generate
constraints about these relations. Finally, it solves the constraints to find out actual definitions of the unknown
relations, thus discovers the lemmas. We have integrated this framework into a prototype prover and have
experimented it on various entailment benchmarks. The experimental results show that our lemma-synthesisassisted prover can prove many entailments that could not be handled by existing techniques. This new
proposal opens up more opportunities to automatically reason with complex inductive heap predicates.
CCS Concepts: • Theory of computation → Logic and verification; Proof theory; Automated reasoning; Separation logic; • Software and its engineering → Software verification;
Additional Key Words and Phrases: Separation logic, entailment proving, mathematical induction, structural
induction, lemma synthesis, proof theory, automated reasoning
ACM Reference Format:
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2018. Automated Lemma Synthesis
in Symbolic-Heap Separation Logic. Proc. ACM Program. Lang. 2, POPL, Article 9 (January 2018), 42 pages.
https://doi.org/10.1145/3158097
∗ The

first and the second author contributed equally.

Authors’ addresses: Quang-Trung Ta, Department of Computer Science, School of Computing, National University of
Singapore, Singapore, taqt@comp.nus.edu.sg; Ton Chanh Le, Department of Computer Science, School of Computing,
National University of Singapore, Singapore, chanhle@comp.nus.edu.sg; Siau-Cheng Khoo, Department of Computer Science,
School of Computing, National University of Singapore, Singapore, khoosc@comp.nus.edu.sg; Wei-Ngan Chin, Department
of Computer Science, School of Computing, National University of Singapore, Singapore, chinwn@comp.nus.edu.sg.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and
the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2018 Copyright held by the owner/author(s).
2475-1421/2018/1-ART9
https://doi.org/10.1145/3158097

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:2
1

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
INTRODUCTION

Having been actively developed in the recent two decades, separation logic appears as one of the
most popular formalisms in verifying the memory-safety property of computer programs [O’Hearn
et al. 2001; Reynolds 2002]. It combines spatial operations, which describe the separation of the
memory, and inductive heap predicates to expressively model the shape of complex data structures,
such as variants of linked lists, trees, or graphs. This modeling has been successfully realized in
both academic research and industrial use. For example, it is implemented by the static analysis
tools SLAYer [Berdine et al. 2011] and Infer [Calcagno et al. 2015] to find memory bugs in system
code or mobile applications in large scale.
Both SLAYer and Infer employ a logic fragment called symbolic-heap separation logic, which differentiates spatial formulas describing the memory shape of a program’s states from pure formulas
representing Boolean constraints of the program’s variables. This fragment is also utilized by
other academic verification systems such as HIP [Chin et al. 2012], jStar [Distefano and Parkinson
2008], and Smallfoot [Berdine et al. 2005a]. Primarily, the verification of a program in such systems
involves three phases: (i) specifying desired properties of the program using separation logic, (ii)
analyzing the program’s behavior against its specification to obtain a set of verification conditions,
mostly in the form of separation logic entailments, and (iii) proving the collected entailments to
determine whether the program behaves accordingly to its specification.
There have been several efforts to prove separation logic entailments, and one of the biggest
challenges is to effectively handle their inductive heap predicates. A commonly practised approach
is to restrict the predicates to only certain classes, such as: predicates whose syntax and semantics
are defined beforehand [Berdine et al. 2004, 2005b; Bozga et al. 2010; Pérez and Rybalchenko 2011,
2013; Piskac et al. 2013, 2014], predicates describing only variants of linked lists [Enea et al. 2014], or
predicates satisfying the particular bounded tree width property [Iosif et al. 2013, 2014]. On the one
hand, such predicate restrictions lead to the invention of effective entailment proving techniques;
on the other hand, they prevent the predicates from modeling complex constraints, which involve
not only the shape, but also the size or the content of data structures.
A more general approach to handle inductive heap predicates is to use proof techniques which are
similar to or based on mathematical induction. These techniques include cyclic proof [Brotherston
et al. 2011], structural induction proof [Chu et al. 2015], and mutual induction proof [Ta et al.
2016]. In general, induction-based techniques are capable of reasoning about structures which
are recursively defined [Bundy 2001]. Therefore, they can be used to deal with inductive heap
predicates in separation logic entailments. However, it is well-known that the induction-based proof
techniques are incomplete, due to the failure of cut-elimination in inductive theories. Consequently,
their successes often depend on an eureka step: discovering supporting lemmas [Bundy 2001].
Not only are the supporting lemmas directly important to induction-based proof systems, but they
are also highly needed by verification systems that use non-induction-based back-end provers, as in
the works of Nguyen and Chin [2008] and Qiu et al. [2013]. These systems cannot automatically
discover the desired lemmas but require the users to manually provide them. Consequently, the
aforementioned verification systems are not fully automated.
Although any valid entailment can become a lemma, the lemmas that are really important are the
ones that can convert between inductive heap predicates, or can combine many inductive heap
predicates into another one, or can split an inductive heap predicate into a combination of many
others. These lemmas are helpful for rearranging inductive heap predicates in a goal entailment
so that the entailment proof can be quickly discovered. They are also called inductive lemmas, as
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:3

induction proofs are often needed to prove them, i.e., there are derivation steps that record and
apply induction hypotheses in the lemmas’ proofs.
In this work, we propose a novel framework to automatically synthesize inductive lemmas to assist in
proving entailments in the fragment of symbolic-heap separation logic. Our framework is developed
based on structural induction proof and template-based constraint solving. Given a goal entailment,
the framework first analyzes the entailment’s heap structure to identify essential lemma templates. It
then sets up unknown relations among each template’s variables and conducts structural induction
proof to generate constraints about the relations. Finally, it solves the constraints to find out actual
definitions of the unknown relations, thus discovers the desired inductive lemmas.
In summary, our work makes the following contributions:
– We propose a novel framework to automatically synthesize lemmas to assist in proving entailments in the fragment of symbolic-heap separation logic with inductive heap predicates.
– We integrate the lemma synthesis framework into an entailment proof system, which allows
the lemmas to be flexibly discovered on-the-fly to support the entailment proofs.
– We implement a prototype prover and experiment it with numerous entailments from various
benchmarks. The experimental result is promising since our tool can prove most of the valid
entailments in these benchmarks and outperforms all existing separation logic provers.
2

MOTIVATING EXAMPLE

In this section, we present a running example to illustrate our work and result. Here, we consider an
inductive heap predicate dll and its variant dllrev, both modeling a doubly linked list data structure
with a length property.
dll(hd, pr , tl, nt, len)

def

=

hd7→pr , nt ∧ hd=tl ∧ len=1
∨ ∃u.(hd7→pr, u ∗ dll(u, hd, tl, nt, len−1))

dllrev(hd, pr , tl, nt, len)

def

=

hd7→pr , nt ∧ hd=tl ∧ len=1
∨ ∃u.(dllrev(hd, pr , u, tl, len−1) ∗ tl7→u, nt)

Each element in the linked list is modeled by a singleton heap predicate x7→pr, nt, where x is
its memory address, pr and nt respectively point to the previous and the next element in the list.
Moreover, both dll(hd, pr, tl, nt, len) and dllrev(hd, pr, tl, nt, len) denote a non-empty doubly linked
list from the first element pointed-to by hd (head) to the last element pointed-to by tl (tail). The
previous and the next element of the entire list are respectively pointed-to by pr and nt, and len
denotes the linked list’s length. The only difference of the two predicates is that dll is recursively
defined from the linked list’s head to the tail, whereas dllrev is defined in the reversed direction.
Suppose that when verifying a program manipulating the doubly linked list data structure, a verifier
needs to prove an entailment relating to an extraction of the last element from a concatenation of
two linked lists with certain constraints on their lengths, such as the following entailment E 1 .
E 1 ≜ dllrev(x, y, u, v, n) ∗ dll(v, u, z, t, 200) ∧ n≥100 |− ∃r .(dll(x, y, r , z, n+199) ∗ z7→r , t)

Unfortunately, the existing entailment proving techniques could not prove E 1 . Specifically, the
predicate-restriction approaches either consider only singly linked list [Berdine et al. 2005b; Bozga
et al. 2010; Cook et al. 2011; Pérez and Rybalchenko 2011, 2013], or do not handle linear arithmetic
constraints [Enea et al. 2014; Iosif et al. 2013, 2014], or require a pre-defined translation of heap
predicates into other theories [Piskac et al. 2013, 2014]. Moreover, the non-induction-based approaches require users to provide supporting lemmas [Chin et al. 2012]. Finally, the induction-based
techniques [Brotherston et al. 2011; Chu et al. 2015] fail to prove E 1 because this entailment is not
general enough to be an effective induction hypothesis, due to its specific constant values.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:4

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

We briefly explain the failure of induction proof on E 1 as follows. Typically, induction is performed on
an inductive heap predicate in E 1 ’s antecedent. Suppose the chosen predicate is dllrev(x, y, u, v, n);
E 1 is then recorded as an induction hypothesis H , whose variables are renamed to avoid confusion:
H ≜ dllrev(a, b, p, q, m) ∗ dll(q, p, c, d, 200) ∧ m≥100 |− ∃k.(dll(a, b, k, c, m+199) ∗ c7→k, d)

Subsequently, the predicate dllrev(x, y, u, v, n) of E 1 is unfolded by its recursive definition to derive
new sub-goal entailments. We consider an interesting case when the below entailment E 1′ is obtained
from an inductive case unfolding of dllrev(x, y, u, v, n):
E 1′ ≜ dllrev(x, y, w, u, n−1) ∗ u7→w, v ∗ dll(v, u, z, t, 200) ∧ n≥100 |− ∃r .(dll(x, y, r, z, n+199) ∗ z7→r, t)

When applying the induction hypothesis H to prove E 1′ , the predicates of the same symbols (dllrev or
dll) in the antecedents of H and E 1′ need to be unified by a substitution. However, such substitution
does not exist since q is mapped to u when unifying dllrev(a, b, p, q, m) vs. dllrev(x, y, w, u, n−1),
whereas q is mapped to the different variable v when unifying dll(q, p, c, d, 200) vs. dll(v, u, z, t, 200).
Alternatively, we can weaken the spatial formula u7→w, v ∗ dll(v, u, z, t, 200) of E 1′ ’s antecedent into
dll(u, w, z, t, 201), w.r.t. the definition of dll, to derive a new entailment E 1′′:
E 1′′ ≜ dllrev(x, y, w, u, n−1) ∗ dll(u, w, z, t, 201) ∧ n≥100 |− ∃r .(dll(x, y, r , z, n+199) ∗ z7→r , t)

Again, no substitution can unify the antecedents of H and E 1′′. For example, the substitution θ 1 ≜
[x/a, y/b, w/p, u/q, n−1/m] might be able to unify dllrev(a, b, p, q, m) with dllrev(x, y, w, u, n−1),
that is, dllrev(a, b, p, q, m)θ 1 ≡ dllrev(x, y, w, u, n−1). However, the constraint n≥100 in the antecedent of E 1′′ cannot prove that n−1≥100, which is obtained from applying θ 1 on the constraint
m≥100 of H . In addition, the substitution θ 2 ≜ [u/q, w/p, z/c, t/d] could not unify dll(q, p, c, d, 200)
with dll(u, w, z, t, 201) since the two constants 201 and 200 are non-unifiable. In short, the above
inability in unifying heap predicates makes induction proof fail on E 1 .
Nevertheless, the entailment E 1 is provable if necessary lemmas can be discovered. For instance,
the following lemmas L 1 , L 2 , and L 3 can be introduced to assist in proving E 1 . More specifically,
L 1 converts a linked list modeled by the predicate symbol dllrev into a linked list modeled by the
variant predicate dll; L 2 combines two linked lists modeled by dll into a new one (similar in spirit to
the “composition lemma” introduced by Enea et al. [2015]); lastly, L 3 splits a linked list modeled by
dll into two parts including a new linked list and a singleton heap:
L1
L2
L3

≜
≜
≜

dllrev(a, b, c, d, m) |− dll(a, b, c, d, m)
dll(a, b, p, q, m) ∗ dll(q, p, c, d, l) |− dll(a, b, c, d, m + l)
dll(a, b, c, d, m) ∧ m≥2 |− ∃w.(dll(a, b, w, c, m−1) ∗ c7→w, d)

The three lemmas L 1 , L 2 , and L 3 can be used to prove E 1 as shown in Figure 1. They are successively
utilized by the lemma application rules LML , LMR to finally derive a new entailment E 4 , which can
be easily proved by standard inference rules in separation logic. We will explain the details of these
lemma application rules LML , LMR and other inference rules in Section 4.1.
|−
n≥100 |− (x=x ∧ y=y ∧ z=z ∧ t=t ∧ n+200=n+200) Π
∗P
E 4 ≜ dll(x, y, z, t, n+200) ∧ n≥100 |− dll(x, y, z, t, n+200)
LMR with L 3 and θ 3
E 3 ≜ dll(x, y, z, t, n+200) ∧ n≥100 |− ∃r .(dll(x, y, r , z, n+199) ∗ z7→r , t)
LML with L 2 and θ 2
E 2 ≜ dll(x, y, u, v, n) ∗ dll(v, u, z, t, 200) ∧ n≥100 |− ∃r .(dll(x, y, r , z, n+199) ∗ z7→r , t)
LML with L 1 and θ 1
E 1 ≜ dllrev(x, y, u, v, n) ∗ dll(v, u, z, t, 200) ∧ n≥100 |− ∃r .(dll(x, y, r , z, n+199) ∗ z7→r , t)

Fig. 1. Proof tree of E 1 using the lemmas L 1 , L 2 , and L 3 , with the substitutions θ 1 ≡ [x/a, y/b, u/c, v/d, n/m],
θ 2 ≡ [x/a, y/b, u/p, v/q, n/m, z/c, t/d, 200/l], and θ 3 ≡ [x/a, y/b, z/c, t/d, r /w, n+200/m]
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:5

In the proof tree in Figure 1, the entailment E 1 can only be concluded valid if all the lemmas L 1 ,
L 2 , and L 3 are also valid. Furthermore, this proof tree is not constructed by any induction proofs.
Instead, induction is performed in the proof of each lemma. We illustrate a partial induction proof
tree of L 1 in Figure 2, where an induction hypothesis is recorded by the induction rule ID and is
later utilized by the induction hypothesis application rule IH. As discussed earlier in Section 1, these
three lemmas are called inductive lemmas. In general, the inductive lemmas help to modularize
the proof of a complex entailment like E 1 : induction is not directly performed to prove E 1 ; it is
alternatively utilized to prove simpler supporting lemmas such as L 1 , L 2 , and L 3 . This modularity,
therefore, increases the success chance of proving complex entailments.
|−Π
true |− ∃t .(v=t ∧ a=a ∧ c=c ∧ d=d ∧ m−1=m−1)
∗P
dll(v, a, c, d, m−1) |− ∃t .(dll(t, a, c, d, m−1) ∧ v=t)
IH(2)
dll(v, a, u, c, m−2) ∗ c7→u, d |− ∃t .(dll(t, a, c, d, m−1) ∧ v=t)
∗7→
a7→b, v ∗ dll(v, a, u, c, m−2) ∗ c7→u, d |− ∃t .(a7→b, t ∗ dll(t, a, c, d, m−1))
PR
...
a7→b, v ∗ dll(v, a, u, c, m−2) ∗ c7→u, d |− dll(a, b, c, d, m)
...
ID(2)
PR
dll(a, b, u, c, m−1) ∗ c7→u, d |− dll(a, b, c, d, m)
a7→b, d ∧ a=c ∧ m=1
IH(1)
|− dll(a, b, c, d, m)
dllrev(a, b, u, c, m−1) ∗ c7→u, d |− dll(a, b, c, d, m)
ID(1)
L 1 ≜ dllrev(a, b, c, d, m) |− dll(a, b, c, d, m)

Fig. 2. Partial induction proof tree of the inductive lemma L 1
where ID(1), ID(2) are performed on dllrev(a, b, c, d, m), dll(a, b, u, c, m−1) to obtain IHs H 1 , H 2 ,
IH(1) with H 1 ≜ dllrev(a ′, b ′, c ′, d ′, m ′ ) |− dll(a ′, b ′, c ′, d ′, m ′ ) and θ 1 ≡ [a/a ′, b/b ′, u/c ′, c/d ′, m−1/m ′ ],
IH(2) with H 2 ≜ dll(a ′, b ′, u ′, c ′, m ′ −1)∗c ′ 7→u ′, d ′ |− dll(a ′, b ′, c ′, d ′, m ′ ), θ 2 ≡ [v/a ′, a/b ′, u/u ′, c/c ′, d/d ′, m−1/m ′ ]

On the other hand, we are not interested in trivial lemmas, which can be proved directly without using
any induction hypotheses: the rule IH is not used in their proofs. For example, L 3′ ≜ dll(a, b, c, d, m)∧
m≥2 |− ∃w.(a7→b, w ∗ dll(w, a, c, d, m−1)) is a trivial lemma, whose direct proof tree is presented
in Figure 3. Obviously, if a trivial lemma can be applied to prove an entailment, then the same
sequence of inference rules utilized in the lemma’s proof can also be directly applied to the goal
entailment. For this reason, the trivial lemmas do not help to modularize the induction proof.
|−Π
m≥2 |− ∃w.(u=w ∧ a=a ∧ c=c ∧ d=d ∧ m−1=m−1)
∗P
dll(u, a, c, d, m−1) ∧ m≥2 |− ∃w.(dll(w, a, c, d, m−1) ∧ u=w)
a7→b, d ∧ a=c ∧ m=1 ∧ m≥2 |−
∗7→
∃w.(a7→b, w ∗ dll(w, a, c, d, m−1))
a7→b, u ∗ dll(u, a, c, d, m−1)∧ m≥2 |−∃w.(a7→b, w ∗ dll(w, a, c, d, m−1))
ID
L 3′ ≜ dll(a, b, c, d, m) ∧ m≥2 |− ∃w.(a7→b, w ∗ dll(w, a, c, d, m−1))

⊥2L

Fig. 3. Direct proof tree of the trivial lemma L 3′

In this work, we propose a novel framework to synthesize inductive lemmas, such as L 1 , L 2 , and L 3 ,
to assist in proving separation logic entailments. For a given goal entailment E, we first identify
all possible lemma templates, which essentially are entailments constructed from heap predicate
symbols appearing in E. The templates will be refined with more Boolean constraints on their
variables until valid inductive lemmas are discovered. We will explain the details in Section 5.
3

THEORETICAL BACKGROUND

Our lemma synthesis framework is developed to assist in proving entailments in the fragment of
symbolic-heap separation logic with inductive heap predicates and linear arithmetic. This fragment
is similar to those introduced in [Albarghouthi et al. 2015; Brotherston et al. 2011, 2016; Ta et al.
2016]. It is also extended with unknown relations to represent Boolean constraints of the desired
lemmas. We will present related background of the entailment proof in the following subsections.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:6

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

3.1

Symbolic-heap separation logic with unknown relations

Syntax. We denote our symbolic-heap separation logic fragment with inductive heap predicates and
unknown relations as SLU
ID and present its syntax in Figure 4. In particular, x is a variable; c and e are
respectively an integer constant and an integer expression1 ; nil is a constant denoting a dangling
memory address (null) and a is a spatial expression modeling a memory address. Moreover, σ denotes
a spatial atom, which is either (i) a predicate emp modeling an empty memory, (ii) a singleton heap
ι
predicate x 7→x 1 , . . . , x n describing an n-field data structure of sort ι in the memory, pointed-to by
x, and having x 1 , . . . , x n as values of its fields2 , or (iii) an inductive heap predicate P(x 1 , . . . , x n )
modeling a recursively defined data structure (Definition 3.1). These spatial atoms constitute a
spatial formula Σ via the separating conjunction operator ∗. On the other hand, π denotes a pure
atom comprising equality constraints among spatial expressions and linear arithmetic constraints
among integer expressions. These pure atoms compose a pure formula Π using standard first-order
logic connectives and quantifiers. Moreover, Π may contain an unknown relation U (Definition 3.4).
We will utilize the unknown relation in various phases of the lemma synthesis.
e
a
π

F
F
F

σ
Π
Σ
F

F
F
F
F

c | x | − e | e1 + e2 | e1 − e2 | c e
nil | x
true | false | a 1 = a 2 | a 1 , a 2 | e 1 = e 2 | e 1 , e 2 | e 1 > e 2 | e 1 ≥ e 2 | e 1 < e 2 | e 1 ≤ e 2
ι
emp | x 7→x 1 , . . . , x n | P(x 1 , . . . , x n )
π | U (x 1 , . . . , x n ) | ¬Π | Π 1 ∧ Π 2 | Π 1 ∨ Π 2 | Π 1 → Π 2 | ∀x .Π | ∃x .Π
σ | Σ1 ∗ Σ2
Σ | Π | Σ ∧ Π | ∃x . F
Fig. 4. Syntax of formulas in SLU
ID

Definition 3.1 (Inductive heap predicate). [Ta et al. 2016] A system of k inductive heap predicates Pi
of arity ni , with i = 1, . . . , k, is defined as follows:


Pi (x 1i , . . . , x ni i )

=

def

k

i (x i , . . . , x i )
F 1i (x 1i , . . . , x ni i ) ∨ . . . ∨ Fm
ni i = 1
i
1
def

where F ji is a definition case of Pi . This fact is also denoted by F ji (x 1i , . . . , x ni i ) ⇒ Pi (x 1i , . . . , x ni i ),
with 1 ≤ j ≤ mi . Moreover, F ji is a base case if it does not contain any predicates recursively defined
with Pi ; otherwise, it is an inductive case.
Example 3.2. The two predicates dll(hd, pr , tl, nt, len) and dllrev(hd, pr , tl, nt, len) in Section 2 are
two examples of inductive heap predicates. Moreover, their definitions are self-recursively defined.
Example 3.3. The two predicates ListE and ListO [Brotherston et al. 2011] are mutually recursively
defined to model linked list segments which respectively contain even and odd number of elements.
(1) ListO(x, y) = x7→y ∨ ∃u.(x7→u ∗ ListE(u, y))
def

(2) ListE(x, y) = ∃u.(x7→u ∗ ListO(u, y))
def

Definition 3.4 (Unknown relation). An unknown relation U (u 1 , . . . ., un ) is an n-ary pure predicate
in first-order logic, whose definition is undefined.
Semantics. Figure 5 exhibits the semantics of formulas in SLU
ID . Given a set Var of variables, Sort
of sorts, Val of values, Loc of memory addresses (Loc ⊂ Val), a model of a formula consists of: a
stack model s, which is a function s: Var → Val, and a heap model h, which is a partial function
h: (Loc × Sort) ⇀ Val+ . We write ⟦Π⟧s to denote the valuation of a pure formula Π under the stack
model s. Moreover, dom(h) denotes the domain of h; h # h ′ indicates that h and h ′ have disjoint
1 We

write c e to denote the multiplication by constant in linear arithmetic.
sort ι represents a unique data type. For brevity, we omit using it when presenting the motivating example.

2 Each

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:7

domains, i.e., dom(h) ∩ dom(h ′) = ∅; and h ◦ h ′ is the union of two disjoint heap models h and h ′.
Besides, [f | x:y] is a function like f except that it returns y for the input x. To define the semantics
of the inductive heap predicates, we follow the standard least fixed point semantics by interpreting
an inductive predicate symbol P as the least prefixed point ⟦P⟧ of a monotone operator constructed
from its inductive definition. The construction is standard and can be found in many places, such
as [Brotherston and Simpson 2011].
s, h |= Π
s, h |= emp
s, h
s, h
s, h
s, h
s, h

ι
|= x 7→x 1 , ..., x n

|= P(x 1 , ..., x n )
|= Σ1 ∗ Σ2
|= Σ ∧ Π
|= ∃x . F

iff
iff

⟦Π⟧s = true and dom(h) = ∅
dom(h) = ∅

iff
iff
iff
iff
iff

dom(h) = {s(x)} and h(s(x), ι) = (s(x 1 ), ..., s(x n ))
(h, ⟦x 1 ⟧s , ..., ⟦x n ⟧s ) ∈ ⟦P⟧
∃h 1 , h 2 : h 1 # h 2 and h 1 ◦ h 2 = h and s, h 1 |= Σ1 and s, h 2 |= Σ2
⟦Π⟧s = true and s, h |= Σ
∃v ∈ Val : [s | x:v], h |= F

Fig. 5. Semantics of formulas in SLU
ID

Entailments. Given the syntax and semantics of formulas, we can define entailments as follows.
This definition is similar to those in separation logic’s literature, such as [Berdine et al. 2004].
Definition 3.5 (Entailment). An entailment between two formulas F 1 and F 2 , denoted as F 1 |− F 2 , is
said to be valid, iff s, h |= F 1 implies that s, h |= F 2 , for all models s, h. Formally,
F 1 |− F 2 is valid, iff ∀s, h. (s, h |= F 1 → s, h |= F 2 )
Here, F 1 and F 2 are respectively called the antecedent and the consequent of the entailment. In
general, separation logic entailments satisfy a transitivity property as stated in Theorems 3.6.
Theorem 3.6 (Entailment transitivity). Given two entailments F 1 |− ∃®
x .F 2 and F 2 |− F 3 , where x®
is a list of variables. If both of them are valid, then the entailment F 1 |− ∃®
x .F 3 is also valid.
x .F 2 is valid, it follows that
Proof. Consider an arbitrary model s, h such that s, h |= F 1 . Since F 1 |− ∃®
s, h |= ∃®
x .F 2 . By the semantics of SLU
’s
formulas,
s
can
be
extended
with
values v® of x® to obtain
ID
s ′ = [s | x:
® v]
® such that s ′, h |= F 2 . Since F 2 |− F 3 is valid, it follows that s ′, h |= F 3 . Since s ′ = [s | x:
® v],
®
|= ∃®
it is implied by the semantics of SLU
’s
formulas
again
that
s,
h
x
.F
.
We
have
shown
that
for
3
ID
x .F 3 . Therefore, F 1 |− ∃®
x .F 3 is valid.
□
an arbitrary model s, h, if s, h |= F 1 , then s, h |= ∃®
Substitution. We write [e 1 /v 1 , . . . , en /vn ], or θ for short, to denote a simultaneous substitution;
and F [e 1 /v 1 , . . . , en /vn ] denotes a formula that is obtained from F by simultaneously replacing all
occurrences of the variables v 1 , . . . , vn by the expressions e 1 , . . . , en . The simultaneous substitution,
or substitution for short, has the following properties, given that FV(F ) and FV(e) are lists of all
free variables respectively occurring in the formula F and the expression e.
Proposition 3.7 (Substitution law for formulas [Reynolds 2008]). Given a separation logic
formula F and a substitution θ ≡ [e 1 /v 1 , . . . , en /vn ]. Let s, h be a separation logic model, where dom(s)
contains (FV(F ) \ {v 1 , . . . , vn }) ∪ FV(e 1 ) ∪ . . . ∪ FV(en ), and let ŝ = [s | v 1 : ⟦e 1 ⟧s | . . . | vn : ⟦en ⟧s ].
Then s, h |= Fθ if and only if ŝ, h |= F
Theorem 3.8 (Substitution law for entailments). Given a separation logic entailment F 1 |− F 2
and a substitution θ . If F 1 |− F 2 is valid, then F 1θ |− F 2θ is also valid.
Proof. Suppose that θ ≡ [e 1 /v 1 , . . . , en /vn ]. Consider an arbitrary model s, h such that s, h |= F 1θ .
Let ŝ = [s | v 1 : ⟦e 1 ⟧s | . . . | vn : ⟦en ⟧s ]. By Proposition 3.7, s, h |= F 1θ implies that ŝ, h |= F 1 . Since
F 1 |− F 2 is valid, it follows that ŝ, h |= F 2 . By Proposition 3.7 again, s, h |= F 2θ . We have shown that
for an arbitrary model s, h, if s, h |= F 1θ , then s, h |= F 2θ . Therefore, F 1θ |− F 2θ is valid.
□
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:8

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

Unknown entailments and unknown assumptions. Recall that we propose to synthesize lemmas by firstly discovering essential lemma templates and then refining them. The template refinement is conducted in 3 steps: (i) creating unknown entailments, which contain unknown relations
representing the lemmas’ desired pure constraints, (ii) proving the entailments by induction and
collecting unknown assumptions about the relations, and (iii) solving the assumptions to discover
the lemmas. We formally define the unknown entailments and the unknown assumptions as follows.
Definition 3.9 (Unknown entailment). An entailment F 1 |− F 2 is called an unknown entailment if the
antecedent F 1 or the consequent F 2 contains an unknown relation U (®
x).
Definition 3.10 (Unknown assumption). A pure implication Π 1 → Π 2 is called an unknown assumption
of the unknown relation U (®
x) if U (®
x) occurs in at least one of the two pure formulas Π 1 and Π 2 .
Syntactic equivalence. An entailment induction proof often contains a step that finds a substitution to unify the antecedents of an induction hypothesis and of the goal entailment. In this work,
we syntactically check the unification between two spatial formulas by using a syntactic equivalence
relation defined earlier in [Ta et al. 2016]. We formally restate this relation in the below.
Definition 3.11 (Syntactic equivalence [Ta et al. 2016]). The syntactical equivalence relation of two
spatial formulas Σ1 and Σ2 , denoted as Σ1  Σ2 , is inductively defined as follows:
ι

ι

(1) emp  emp
(2) u 7→v 1 , . . . , vn  u 7→v 1 , . . . , vn
(3) P(u 1 , . . . , un )  P(u 1 , . . . , un )
(4) (Σ1  Σ1′ ) ∧ (Σ2  Σ2′ ) → (Σ1 ∗ Σ2  Σ1′ ∗ Σ2′ ) ∧ (Σ1 ∗ Σ2  Σ2′ ∗ Σ1′ )

3.2

Structural induction for entailment proofs and lemma syntheses

We develop the lemma synthesis framework based on a standard structural induction proof. This
proof technique is an instance of Noetherian induction, a.k.a. well-founded induction [Bundy 2001].
We will briefly explain both Noetherian induction and structural induction here. Nonetheless, our
lemma synthesis idea can also be integrated into other induction-based proof techniques.
Noetherian induction. Given P is a conjecture on structures of type τ where ≺τ is a well-founded
relation among these structures, i.e., there is no infinite chain like . . . ≺τ α n ≺τ . . . ≺τ α 1 . Then
the Noetherian induction principle states that: P is said to hold for all these structures, if for any
structure α, the fact that P(β) holds for all structures β ≺τ α implies that P(α) also holds. Formally:
∀α : τ . (∀β : τ ≺τ α . P(β)) → P(α)
∀α : τ . P(α)

Substructural relation. We prove entailments by applying Noetherian induction on the structure
of inductive heap predicates. The substructural relation is formally defined in Definition 3.12.
Definition 3.12 (Substructural relation). A heap predicate P1 (v)
® is said to be a substructure of P2 (®
u),
denoted by P1 (v)
® ≺ P2 (®
u), if P1 (v)
® occurs in a formula obtained from directly unfolding P2 (®
u) or
from unfolding any substructure of P2 (®
u). These conditions are formally stated as follows:
def

(1) ∃w,
® Σ, Π, F (®
u). (F (®
u)  ∃w.(P
® 1 (v)
® ∗ Σ ∧ Π) ∧ F (®
u) ⇒ P2 (®
u))
def
′
®
®
®
®
(2) ∃w,
® Σ, Π, F (t ), P (t ). (F (t )  ∃w.(P
® 1 (v)
® ∗ Σ ∧ Π) ∧ F (t ) ⇒ P ′ (t®) ∧ P ′ (t®) ≺ P2 (®
u))

In the above definition, P1 and P2 can be the same or different predicate symbols. The latter happens
when they are mutually recursively defined, such as ListE and ListO in Example 3.3.
Theorem 3.13 (Well-foundedness). Given an inductive heap predicate P1 (®
u 1 ). If it is satisfiable,
i.e., P1 (®
u 1 ) . false, then under the least fixed point semantics of inductive heap predicates, there is no
infinite chain like . . . ≺ Pn (®
un ) ≺ . . . ≺ P1 (®
u 1 ).
Proof. Suppose that there exists an infinite chain . . . ≺ Pn (®
un ) ≺ . . . ≺ P1 (®
u 1 ). For all i ≥ 1, we can
always insert all predicates derived when unfolding Pi (®
ui ) to obtain Pi+1 (®
ui+1 ) into the current
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:9

chain. Therefore, w.l.o.g., we can assume that Pi+1 (®
ui+1 ) is obtained from directly unfolding Pi (®
ui ),
for all i ≥ 1. Hence, . . . ≺ Pn (®
un ) ≺ . . . ≺ P1 (®
u 1 ) is also the infinite unfolding chain of P1 (®
u 1 ). In the
least fixed point semantics, if a predicate is unfolded infinitely, it can be evaluated to false. Therefore,
P1 (®
u 1 ) ≡ false. This contradicts with the theorem’s hypothesis that P1 (®
u 1 ) is satisfiable.
□
Structural induction. We apply the substructural relation ≺ to propose a structural induction
principle for the entailment proof. Consider an entailment E whose antecedent contains an inductive
predicate P(®
u), that is, E ≜ F 1 ∗P(®
u) |− F 2 , for some formulas F 1 , F 2 . We write E(P(®
u)) to parameterize
E by P(®
u); and E(P(v))
® is an entailment obtained from E(P(®
u)) by replacing P(®
u) by P(v)
® and
respectively replacing variables in u® by variables in v.
® Moreover, we write |= E(P(®
u)) to denote that
E holds for P(®
u). The structural induction principle is formally stated as follows:
Theorem 3.14 (Structural induction). The entailment E(P(®
u)) ≜ F 1 ∗ P(®
u) |− F 2 is valid, if for all
predicate P(®
u), the fact that E holds for all sub-structure predicates P(v)
® of P(®
u) implies that E also
holds for P(®
u). Formally:
∀P(®
u). (∀P(v)
® ≺ P(®
u). |= E(P(v)))
® → |= E(P(®
u))
∀P(®
u). |= E(P(®
u))

Proof. We consider two scenarios w.r.t. P(®
u) in the entailment E(P(®
u)) ≜ F 1 ∗ P(®
u) |− F 2 as follows.
(1) If P(®
u) ≡ false. Then F 1 ∗ P(®
u) ≡ false, therefore E(P(®
u)) is valid. (2) If P(®
u) . false. Then by
Theorem 3.13, the substructural relation ≺, which applies to P(®
u), is well-founded. In this scenario,
the above induction principle is an instance of the Noetherian induction [Bundy 2001] where the
substructural relation ≺ is chosen as the well-founded relation. Therefore, the correctness of this
theorem is automatically implied by the soundness of the Noetherian induction principle.
□
4

THE STRUCTURAL INDUCTION PROOF SYSTEM

In this section, we present a structural induction proof system for separation logic entailments.
Initially, this system aims to prove normal entailments using a set of inference rules (Section 4.1).
These rules include the two lemma application rules which apply synthesized lemmas to assist in
proving entailments (Figure 8). We use the same proof system to reason about unknown entailments,
introduced in the lemma synthesis, using a set of synthesis rules (Section 4.2). The proof system
also includes a proof search procedure which selectively applies the aforementioned rules to prove
a goal entailment (Section 4.3). We will explain the details in the following sections.
4.1

Inference rules for standard entailments

Each inference rule of our proof system contains zero or more premises, a conclusion, and possibly
a side condition. The premises and the conclusion are in the form of H, L, F 1 |− F 2 , where H and
L are respectively sets of induction hypotheses and valid lemmas, and F 1 |− F 2 is the (sub-)goal
entailment. An inference rule can be interpreted as follows: if all entailments in its premises are
valid, and its side condition (if present) is satisfied, then its goal entailment is also valid.
For brevity, we write F to denote a symbolic-heap formula ∃®
x .(Σ ∧ Π), where x® is a list of quantified
variables (possibly empty). Furthermore, we define F ∗ Σ ′ ≜ ∃®
x .(Σ ∗ Σ ′ ∧ Π) and F ∧ Π ′ ≜
′
′
′
∃®
x .(Σ ∧ Π ∧ Π ), given that FV(Σ ) ∩ x® = ∅ and FV(Π ) ∩ x® = ∅. We also write u® = v® to denote
(u 1 = v 1 ) ∧ . . . ∧ (un = vn ), given that u® ≜ u 1 , . . . , un and v® ≜ v 1 , . . . , vn are two variable lists of the
same size. Finally, u® # v® indicates that the two lists u® and v® are disjoint, i.e., ∄w.(w ∈ u® ∧ w ∈ v).
®
The set of inference rules comprises logical rules (Figure 6) reasoning about the logical structure of
the entailments, induction rules (Figure 7) proving the entailments by structural induction, and
lemma application rules (Figure 8) applying supporting lemmas to assist in proving the entailments.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:10

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

⊥1L
=L
∃L
∃R

PR

ι1

ι2

H, L, F 1 ∗ u 7→v® ∗ u 7→t® |− F 2

⊥2L

EL

H, L, F 1 ∧ u=v |− F 2
H, L, F 1 [u/x] |− F 2

|−Π

H, L, Π1 |− Π2

H, L, F 1 |− ∃®
x .(F 2 ∗ emp)
H, L, F 1 ∧ ¬Π |− F 2
H, L, F 1 ∧ Π |− F 2

CA

H, L, F 1 |− ∃®
x .F 2 [u/v]
H, L, F 1 |− ∃®
x, v.(F 2 ∧ u=v)
x .(F 2 ∗ FiP (®
u))
H, L, F 1 |− ∃®

H, L, F 1 |− F 2

∗7→

def

Π1 →Π2

H, L, F 1 |− ∃®
x .F 2

ER

H, L, F 1 ∗ emp |− F 2

u < FV(F 2 )

H, L, F 1 |− ∃®
x .(F 2 ∗ P(®
u))

Π1 →false

H, L, F 1 |− F 2

H, L, F 1 [u/v] |− F 2 [u/v]

H, L, ∃x .F 1 |− F 2

H, L, F 1 ∧ Π 1 |− F 2

F iP (u)
® ⇒ P(u)
®

∗P

H, L, F 1 |− ∃®
x .(F 2 ∧ u=t ∧ v=
® w)
®
ι

ι

H, L, F 1 ∗ u 7→v® |− ∃®
x .(F 2 ∗ t 7→w)
®
H, L, F 1 |− ∃®
x .(F 2 ∧ u=
® v)
®
H, L, F 1 ∗ P(®
u) |− ∃®
x .(F 2 ∗ P(v))
®

u < x,
® v® # x®

u® # x®

Fig. 6. Logical rules

Logical rules. The set of logical rules in Figure 6 consists of:
• Axiom rules |−Π , ⊥1L , ⊥2L . These rules prove pure entailments by invoking an off-the-shelf prover
such as Z3 [Moura and Bjørner 2008] (as in the rule |−Π ), or prove entailments whose antecedents
ι1
ι2
are inconsistent, i.e., they contain overlaid singleton heaps (u 7→v® and u 7→t® in the rule ⊥1L ) or
contradictions (Π 1 → false in the rule ⊥2L ).
• Normalization rules ∃L , ∃R , =L , EL , ER . These rules simplify the goal entailment by either eliminating existentially quantified variables (∃L , ∃R ), or removing equalities (=L ) or empty heap
predicates (EL , ER ) from the entailment.
• Case analysis rule CA. This rule performs a case analysis on a pure condition Π by deriving
two sub-goal entailments whose antecedents respectively contain Π and ¬Π. The underlying
principle of this rule is known as the law of excluded middle [Whitehead and Russell 1912].
• Unfolding rule PR . This rule derives a new entailment by unfolding a heap predicate in the goal
entailment’s consequent by its inductive definition.
• Matching rules ∗7→, ∗P. These rules remove identical singleton heap predicates (∗7→) or inductive
heap predicates (∗P) from two sides of the goal entailments. Here, we ensure that these predicates
are identical by adding equality constraints about their parameters into the derived entailments’
consequents.
H ′, L, Σ1 ∗ F 1P (®
u) ∧ Π 1 |− F 2
ID

IH

...

P (®
H ′, L, Σ1 ∗ Fm
u) ∧ Π1 |− F 2

P (u);
P(u)
® = F 1P (u)
® ∨ ... ∨ Fm
® †
def

H, L, Σ1 ∗ P(®
u) ∧ Π 1 |− F 2
† : H ′ ≜ H ∪ {H }, where H is obtained by freshly renaming all variables of Σ1 ∗ P(®
u) ∧ Π1 |− F 2

H ∪ {Σ3 ∗ P(v)
® ∧ Π3 |− F 4 }, L, F 4θ ∗ Σ ∧ Π 1 |− F 2 P(u)
® ≺ P(v);
®
®  Σ3 θ ∗ P(v)θ
® ∗ Σ) ∧ (Π1 →Π3 θ )
H ∪ {Σ3 ∗ P(v)
® ∧ Π 3 |− F 4 }, L, Σ1 ∗ P(®
u) ∧ Π1 |− F 2 ∃θ, Σ.(Σ1 ∗ P(u)
Fig. 7. Induction rules

Induction rules. The structural induction principle is integrated into our proof system via the
two induction rules ID and IH (Figure 7). These rules are explained in details as follows:
• Rule ID. This rule performs the structural induction proof on a chosen heap predicate P(®
u) in
the antecedent of the goal entailment Σ1 ∗ P(®
u) ∧ Π 1 |− F 2 . In particular, the predicate P(®
u) is
def P
P
unfolded by its inductive definition P(®
u) = F 1 (®
u) ∨...∨ Fm (®
u) to derive new sub-goal entailments
as shown in this rule’s premises. Moreover, the goal entailment is also recorded as an induction
hypothesis in the set H ′ so that it can be utilized later to prove the sub-goal entailments.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:11

• Rule IH. This rule applies an appropriate recorded induction hypothesis H ≜ Σ3 ∗P(v)∧Π
®
3 |− F 4
to prove the goal entailment Σ1 ∗ P(®
u) ∧ Π1 |− F 2 . It first checks the well-founded condition P(®
u) ≺
P(v),
® i.e. P(®
u) is a substructure of P(v),
® which is required by the structural induction principle. In
practice, this condition can be easily examined by labeling each inductive heap predicate Q(®
x)
in a proof tree with a set of its ancestor predicates, which are consecutively unfolded to derive
Q(®
x). By that mean, P(®
u) ≺ P(v)
® iff P(v)
® appears in the label of P(®
u). Afterwards, the induction
hypothesis application is performed in two steps:
– Unification step: unify the antecedents of both the goal entailment and the induction hypothesis by syntactically finding a substitution θ and a spatial formula Σ such that Σ1 ∗ P(®
u) 
® ∗ Σ and Π 1 →Π 3θ . If these conditions hold, then it is certain that the entailment
Σ3θ ∗ P(v)θ
E ≜ Σ1 ∗ P(®
u) ∧ Π 1 |− Σ3θ ∗ P(v)θ
® ∗ Σ ∧ Π 3θ ∧ Π 1 is valid.
– Proving step: if such θ and Σ exist, then derive a new sub-goal entailment F 4θ ∗ Σ ∧ Π 1 |− F 2 . We
will explain why this sub-goal entailment is derived. The induction hypothesis Σ3 ∗P(v)∧
® Π 3 |− F 4
implies that Hθ ≜ Σ3θ ∗ P(v)θ
® ∧ Π 3θ |− F 4θ is also valid, by Theorem 3.8. From E and Hθ , we
then have a derivation chain: Σ1 ∗ P(®
u) ∧ Π 1 |− Σ3θ ∗ P(v)θ
® ∗ Σ ∧ Π 3θ ∧ Π 1 |− F 4θ ∗ Σ ∧ Π 1 .
Therefore, if the sub-goal entailment F 4θ ∗ Σ ∧ Π 1 |− F 2 can be proved, then the goal entailment
holds. Here, we propagate the pure condition Π 1 through the chain as we want the antecedent
of the sub-goal entailment to be the strongest in order to prove F 2 .
H, L ∪ {Σ3 ∧ Π 3 |− F 4 }, F 4θ ∗ Σ ∧ Π 1 |− F 2
LML

LMR

H, L ∪ {Σ3 ∧ Π3 |− F 4 }, Σ1 ∧ Π1 |− F 2

∃θ, Σ. (Σ1  Σ3θ ∗ Σ) ∧ (Π1 →Π 3θ )

® 4 ∧ Π4 )}, F 1 |− ∃®
x .(F 3θ ∗ Σ ∧ Π2 )
H, L ∪ {F 3 |− ∃w.(Σ
H, L ∪ {F 3 |− ∃w.(Σ
® 4 ∧ Π 4 )}, F 1 |− ∃®
x .(Σ2 ∧ Π 2 )

∃θ, Σ. (Σ4θ ∗ Σ  Σ2 ) ∧ (wθ
® ⊆ x)
®

Fig. 8. Lemma application rules

Lemma application rules. The two rules LML , LMR in Figure 8 derive a new sub-goal entailment
by applying a lemma on the goal entailment’s antecedent or consequent. In particular:
• The rule LML applies a lemma on the goal entailment’s antecedent. It is similar to the induction
application rule IH, except that we do not need to check the well-founded condition of the
structural induction proof, since the applied lemma is already proved valid.
• The rule LMR applies a lemma on the goal entailment’s consequent. It also needs to perform
an unification step: finding a substitution θ and a formula Σ so that the heap parts of the goal
entailment’s and the lemma’s consequents are unified, i.e., Σ4θ ∗ Σ  Σ2 . If this step succeeds, then
E 1 ≜ Σ4θ ∗Σ∧Π 2 |− Σ2 ∧Π 2 is valid. The lemma F 3 |− ∃w.(Σ
® 4 ∧Π 4 ) implies that F 3 |− ∃w.Σ
® 4 is valid.
|
Hence, F 3θ − ∃wθ
® .Σ4θ is valid by Theorem 3.8, following that F 3θ ∗ Σ ∧ Π 2 |− ∃wθ
® .(Σ4θ ∗ Σ ∧ Π 2 )
is also valid. By the rule’s side condition wθ
® ⊆ x,
® we have another valid entailment E 2 ≜
F 3θ ∗ Σ ∧ Π 2 |− ∃®
x .(Σ4θ ∗ Σ ∧ Π 2 ). Therefore, by proving the entailment F 1 |− ∃®
x .(F 3θ ∗ Σ ∧ Π 2 )
in this rule’s premise and applying Theorem 3.6 twice sequentially on E 2 and then E 1 , we can
conclude that the goal entailment F 1 |− ∃®
x .(Σ2 ∧ Π 2 ) is also valid.
4.2

Synthesis rules for unknown entailments

Figure 9 presents synthesis rules, which deal with unknown entailments introduced in the lemma
synthesis. These rules share the similar structure to the inference rules, except that each of them
also contains a special premise indicating an assumption set A of the unknown relations. We will
describe in details the synthesis rules as follows:
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:12

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

• Axiom synthesis rules U1Π , U2Π , U1Σ , U2Σ . These rules conclude the validity of their unknown goal
entailments under the assumption sets A in the rules’ premises. The rule U1Π and U2Π handle
pure entailments with unknown relations either in the antecedents or the consequents. The
rule U1Σ and U2Σ deal with unknown entailments whose antecedents contain non-empty spatial
formulas while the consequents are pure formulas or vice versa. In both cases, the antecedents
must be inconsistent to make the goal entailments valid. Here, we only create assumptions on
the pure parts, i.e., Π 1 ∧ U (®
x) → false, since inconsistency in their heap parts, if any, can be
detected earlier by the rule ⊥1L . Also, we do not consider the case that the unknown relations
only appear in the consequents since these relations cannot make the antecedents inconsistent.
• Induction hypothesis synthesis rule UIH . This rule applies an induction hypothesis to prove a
derived unknown entailment. The induction hypothesis also contains unknown relations since
it is recorded earlier from an unknown goal entailment. The rule UIH is similar to the normal
induction hypothesis application rule IH, except that it does not contain a side condition like
Π 1 ∧ U (®
x) → (Π 3 ∧ U (®
y))θ , due to the appearance of the unknown relation U . Instead, this
condition will be registered in the unknown assumption set A in the premises of UIH .
A ≜ {Π 1 ∧ U (®
x) → Π2 }

U1Π

U1Σ

H, L, Π1 ∧ U (®
x) |− Π2
A ≜ {Π 1 → ∃w.(Π
® 2 ∧ U (®
x))}

U2Π

U2Σ

H, L, Π1 |− ∃w.(Π
® 2 ∧ U (®
x))

A ≜ {Π 1 ∧ U (®
x) → false}
H, L, Σ1 ∧ Π1 ∧ U (®
x) |− Π2

Σ1 ,emp

A ≜ {Π 1 ∧ U (®
x) → false}
H, L, Π 1 ∧ U (®
x) |− ∃w.(Σ
® 2 ∧ Π2 )

Σ2 ,emp

H ∪ {Σ3 ∗ P(v)
® ∧ Π3 ∧ U (®
y) |− F 4 }, L, F 4θ ∗ Σ ∧ Π1 |− F 2
A ≜ {Π 1 ∧ U (®
x) → (Π 3 ∧ U (®
y))θ }
†
u) ∧ Π1 ∧ U (®
x) |− F 2
H ∪ {Σ3 ∗ P(v)
® ∧ Π 3 ∧ U (®
y) |− F 4 }, L, Σ1 ∗ P(®
with † : P(®
u) ≺ P(v);
® ∃θ, Σ. (Σ1 ∗ P(®
u)  Σ3θ ∗ P(v)θ
® ∗ Σ)

UIH

Fig. 9. Synthesis rules

4.3

The entailment proving procedure

Figure 10 presents the core procedure Prove of our proof system. In particular, the input of Prove
includes an induction hypothesis set H , a valid lemma set L, and a goal entailment F 1 |− F 2 .
These three inputs correlate to an inference step of the proof system. We also use an additional
parameter mode to control when new lemmas can be synthesized (if mode = SynLM) or strictly
not (if mode = NoSyn). The procedure Prove returns the validity of the goal entailment, a set of
new lemmas synthesized during the proof, and a set of assumptions to make the entailment valid.
There are two main contexts where this procedure is initially invoked:
– In the entailment proving phase, Prove is invoked to prove a normal entailment F 1 |− F 2 , which
does not contain any unknown relation, with the initial setting H = ∅, L = ∅, mode = SynLM.
– In the lemma synthesis phase, Prove is invoked either to prove an unknown entailment F 1 |− F 2
related to a lemma template, or to verify whether a discovered lemma is an inductive lemma. In
the first case, Prove will establish sufficient assumptions about unknown relations appearing
in the entailment so that the entailment can become valid. Moreover, Prove is invoked with
mode = NoSyn in both the two cases to avoid entering into nested lemma synthesis phases.
In Figure 10, we also present formal specifications of Prove in pairs of pre- and post-conditions
(Requires/Ensures). These specifications relate to three cases when Prove is invoked to prove an
unknown entailment with the lemma synthesis always being disabled (mode = NoSyn), or to
prove a normal entailment with the lemma synthesis being disabled (mode = NoSyn) or enabled
(mode = SynLM). We write res to represent the returned result of Prove. In addition, hasU nk(E)
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:13

indicates that the entailment E has an unknown relation, valid(L) and valid(A) mean that all
lemmas in L and all assumptions in A are semantically valid. Moreover, valid ID (H, L, E) specifies
that the entailment E is semantically valid under the induction hypothesis set H and the lemma
set L. We will refer to these specifications when proving the proof system’s soundness. The formal
verification of Prove w.r.t. these specifications is illustrated in Appendix B.
Procedure Prove(H, L, F 1 |− F 2 , mode)
Input: F 1 |− F 2 is the goal entailment, H is a set of induction hypotheses, L is a set of valid lemmas, and
mode controls whether new lemmas will be synthesized (SynLM) or strictly not (NoSyn)
Output: The goal entailment’s validity (Valid⟨ξ ⟩ or Unkn, where ξ is the witness valid proof tree),
a set of new synthesized lemmas, and a set of unknown assumptions
Requires: (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L)
Ensures: (res = (Unkn, ∅, ∅)) ∨ ∃ξ , A.((res = (Valid⟨ξ ⟩, ∅, A)) ∧ (valid(A) → valid ID (H, L, F 1 |−F 2 )))
Requires: (mode = NoSyn) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L)
Ensures: (res = (Unkn, ∅, ∅)) ∨ ∃ξ .((res = (Valid⟨ξ ⟩, ∅, ∅)) ∧ valid ID (H, L, F 1 |−F 2 ))
Requires: (mode = SynLM) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L)
Ensures: (res = (Unkn, ∅, ∅)) ∨ ∃ξ ,Lsyn .((res = (Valid⟨ξ ⟩, Lsyn , ∅)) ∧ valid(Lsyn ) ∧ valid ID (H, L, F 1 |−F 2 ))
1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:

R ← {Unify(R, (H, L, F 1 |− F 2 )) | R ∈ R}
//Find applicable inference and synthesis rules from R
Lsyn ← ∅
//Initialize the new synthesized lemma set
if (mode = SynLM) and NeedLemmas(F 1 |− F 2 , R) then
//Synthesize new lemmas
Lsyn ← SynthesizeLemma(L, F 1 |− F 2 )
R ← R ∪ {Unify(R, (H, Lsyn , F 1 |− F 2 )) | R ∈ {LML , LMR }}
//Update lemma application rules
for each R in R do
A←∅
if IsSynthesisRule(R) then A ← Assumptions(R)

//Initialize the assumption set
//R ∈ {U1Π , U2Π , U1Σ , U2Σ , UIH }

//R ∈ { |−Π , ⊥1L , ⊥2L , U1Π , U2Π , U1Σ , U2Σ }
if IsAxiomRule(R) then
ξ ← CreateWitnessProofTree(F 1 |− F 2 , R, ∅)
return (Valid⟨ξ ⟩, Lsyn , A)
(Hi , Li , F 1i |− F 2i )i = 1...n ← Premises(R)
i ,A )
(r i , Lsyn
//Prove all sub-goals
i i = 1...n ← Prove(Hi , L ∪ Lsyn ∪ Li , F 1i |− F 2i , mode)i = 1...n
if r i = Valid⟨ξ i ⟩ for all i = 1 . . . n then
ξ ← CreateWitnessProofTree(F 1 |− F 2 , R, {ξ 1 , . . . , ξ n })
1 ∪ . . . ∪ Ln , A ∪ A ∪ . . . ∪ A )
return (Valid⟨ξ ⟩, Lsyn ∪ Lsyn
1
n
syn
return (Unkn, ∅, ∅)

//All rules fail to prove F 1 |− F 2

Fig. 10. The main proof search procedure with description (Input/Output) and specification (Requires/Ensures)

Given the goal entailment F 1 |− F 2 , the procedure Prove first finds from all rules R (Figures 6, 7,
8, and 9) a set of potential inference and synthesis rules R, which can be unified with F 1 |− F 2
(line 1). When the lemma synthesis mode is enabled (mode = SynLM), it invokes a subroutine
NeedLemmas to examine the selected rules R and the goal entailment F 1 |− F 2 to decide whether
it really needs to synthesize new lemmas (line 3). Note that the input valid lemma set L is also
exploited to make the lemma synthesis more effective (line 4). The new synthesized lemmas, if any,
will be utilized to discover new lemma application rules (lines 5). Thereafter, Prove successively
applies each rule R ∈ R to derive new sub-goal entailments, as in the premises of R, and recursively
searches for their proofs (line 6 – 16). It returns the valid result (Valid⟨ξ ⟩, where ξ is the witness
proof tree) if the selected rule R does not introduce any new sub-goals (lines 9 – 11), or all derived

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:14

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

sub-goals are successfully proved (line 12 – 16). In essence, the proof tree ξ is composed of a root
(the goal entailment F 1 |− F 2 ), a label (the applied rule R), and sub-trees, if any, corresponding to
the sub-goal entailments’ proofs (lines 10 and 15). Its form is intuitively similar to the proof trees
depicted in Figures 1, 2, and 3. On the other hand, Prove announces the unknown result (Unkn)
when all selected rules in R fail to prove the goal entailment (line 17). Besides, Prove also returns a
set of new synthesized lemmas and a set of unknown assumptions. These lemmas are discovered
when Prove is invoked in the entailment proving phase. The unknown assumptions are collected
by the synthesis rules (line 8), when Prove is executed in the lemma synthesis phase.
Details of the lemma synthesis will be presented in Section 5. In the following, we will explain
when Prove decides to synthesize new lemmas (line 3). The procedure NeedLemmas returns true
when all the following conditions are satisfied:
– F 1 |− F 2 is not an unknown entailment, which implies that lemmas are possibly needed.
– R does not contain any axiom or normalization ( |−Π , ⊥1L , ⊥2L , ∃L , ∃R , =L , EL , ER ), matching rules
of identical heap predicates (∗7→, ∗P), or unfolding rules that introduce identical predicates
(ID, PR ). This condition indicates that all rules in R cannot make any immediate proof progress.
– R does not have any induction hypothesis or lemma application rules (IH, LML , LMR ), or any
case analysis rule (CA) that potentially leads to the application of an induction hypothesis or a
lemma. This condition conveys that existing induction hypotheses and lemmas are inapplicable
– F 1 |− F 2 is not a good induction hypothesis candidate, which indicates that the induction hypothesis recorded from F 1 |− F 2 cannot be used to prove other derived entailments.
While the first three conditions can be checked syntactically on F 1 |− F 2 and R, the last condition
can be tested by a trial and error method. Specifically, F 1 |− F 2 will firstly be recorded as a temporary
induction hypothesis candidate, and then each inductive heap predicate in F 1 will be consecutively
unfolded to search for an application of the recorded induction hypothesis via the rule IH. If no
induction hypothesis application can be found, then F 1 |− F 2 is evidently not a good candidate.
4.4

Soundness of the proof system

Recall that our proof search procedure Prove is implemented in a recursive manner. When it is
invoked to prove a normal goal entailment E, which does not contain any unknown relation,
the initial setting H = ∅, L = ∅, mode = SynLM indicates that no induction hypothesis or lemma
is provided beforehand, and the proof system can synthesize new lemmas to assist in proving
E. When synthesizing the new supporting lemmas, the proof system can be utilized to prove an
unknown entailment related to a lemma template or to verify a discovered lemma, which is a normal
entailment not containing any unknown relation. In addition, the proof system is also invoked to
prove sub-goal entailments, which are normal entailments derived from E. All of these scenarios
are summarized by the three specifications in Figure 10.
In the following, we present Propositions 4.1, 4.2, and 4.3, which respectively specify the soundness
of our proof system in the three typical scenarios: (i) proving an unknown entailment with the
lemma-synthesis-disabled mode (the first pre/post specification of Prove), (ii) verifying a discovered
lemma, i.e., proving a normal entailment with the lemma-synthesis-disabled mode (the second
pre/post specification), or (iii) proving a normal entailment with the lemma-synthesis-enabled
mode (the third pre/post specification). Finally, we describe the overall soundness of the proof
system in Theorem 4.4 when Prove is invoked with the initial setting H = ∅, L = ∅, mode = SynLM.
Note that Propositions 4.1 and 4.2 are relevant to the lemma synthesis in Section 5. Proposition 4.3
directly relates to the overall soundness in Theorem 4.4.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:15

Proposition 4.1 (Proof of an unknown entailment). Given an unknown entailment E. If the
procedure Prove returns Valid⟨_⟩ and generates an assumption set A when proving E in the lemmasynthesis-disabled mode (NoSyn), using an empty induction hypothesis set (H =∅) and a valid lemma
set L as its inputs, then E is semantically valid, given that all assumptions in A are valid.
Proposition 4.2 (Proof of a normal entailment when the lemma synthesis is disabled).
Given a normal entailment E which does not contain any unknown relation. If the procedure Prove
returns Valid⟨_⟩ when proving E in the lemma-synthesis-disabled mode (NoSyn), using an empty
induction hypothesis set (H =∅) and a valid lemma set L as its inputs, then E is semantically valid.
Proposition 4.3 (Proof of a normal entailment when the lemma synthesis is enabled).
Given a normal entailment E which does not contain any unknown relation. If the procedure Prove returns Valid⟨_⟩ and synthesizes a set of lemmas Lsyn when proving E in the lemma-synthesis-enabled
mode (SynLM), using an empty induction hypothesis set (H =∅) and a valid lemma set L as its inputs,
then the entailment E and all lemmas in Lsyn are semantically valid.
Proofs of Propositions 4.1, 4.2, 4.3. We first show that all inference and synthesis rules are sound,
and the proof system in the NoSyn mode is sound. Based on that, we can prove Propositions 4.1
and 4.2. The proof of Proposition 4.3 will be argued based on the lemma synthesis’s soundness in
Section 5. Details of all these proofs are presented in Appendix A.
□
Theorem 4.4 (The overall soundness of the proof system). Given a normal entailment E which
does not contain any unknown relation, if the procedure Prove returns Valid⟨_⟩ when proving E in
the initial context that there is no induction hypothesis or lemma provided beforehand and the lemma
synthesis is enabled (H = ∅, L = ∅, mode = SynLM), then E is semantically valid.
Proof. Since E does not contain any unknown relation, both the input induction hypothesis set
and lemma set are empty (H =∅, L=∅), and Prove is invoked in the SynLM mode, it follows from
Proposition 4.3 that if Prove returns Valid⟨_⟩ when proving E, then E is semantically valid.
□
5

THE LEMMA SYNTHESIS FRAMEWORK

We are now ready to describe our lemma synthesis framework. It consists of a main procedure,
presented in Subsection 5.1, and auxiliary subroutines, described in Subsections 5.2, 5.3, and 5.4.
Similar to the proof system in Section 4, we also provide the input/output description and the formal
specification for each of these synthesis procedures. We use the same keyword res to represent the
returned result and valid(L) indicates that all lemmas in L are semantically valid.
5.1 The main synthesis procedure
Figure 11 presents the main lemma synthesis procedure (SynthesizeLemma). Its
inputs include a goal entailment F 1 |− F 2
which needs to be proved by new lemmas,
and a set of previously synthesized lemmas L which will be exploited to make
the current synthesis more effective. The
procedure SynthesizeLemma first identifies a set of desired lemma templates
based on the entailment’s heap structure, via the invocation of the procedure
CreateTemplate (line 18). These lemma

Procedure SynthesizeLemma(L, F 1 |− F 2 )
Input: F 1 |−F 2 is the goal entailment, L is a valid lemma set
Output: A set of new synthesized lemmas
Requires: valid(L)
Ensures: valid(res)
18: for each Σ1 |− ∃v.Σ
® 2 in CreateTemplate(L, F 1 |− F 2 ) do
19:
L1 ← RefineAnte(L, Σ1 ∧ true |− Σ2 )
20:
L2 ← RefineConseq(L, Σ1 |− ∃v.Σ
® 2)
21:
if (L1 ∪ L2 ) , ∅ then return (L1 ∪ L2 )
22: return ∅
Fig. 11. The main lemma synthesis procedure

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:16

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

templates are of the form Σ1 |− ∃v.Σ
® 2 , in which Σ1 and Σ2 are spatial formulas constructed from
heap predicate symbols appearing in F 1 and F 2 , respectively, and v® are all free variables in Σ2 . By this
construction, each synthesized lemma will share a similar heap structure with the goal entailment,
hence they can be unified by the lemma application rules LML and LMR . We will formally define
the lemma templates in Subsection 5.2. In our implementation, CreateTemplate returns a list of
possible lemma templates, which are sorted in the ascending order of their simplicity, i.e., templates
containing less spatial atoms are on the top of the list. Moreover, any template sharing the same
heap structure with a previously synthesized lemma in L will not be considered.
The framework then successively refines each potential lemma template by continuously discovering
and adding in pure constraints of its variables until valid inductive lemmas are found. In essence,
for a given lemma template, the refinement is performed by a 3-step recipe:
(1) Establishing an unknown relation representing a desired constraint inside the template and
creating an unknown entailment.
(2) Proving the unknown entailment by structural induction and collecting assumptions about
the unknown relation.
(3) Solving the assumptions to find out the actual definition of the unknown relation, thus
discovering the desired inductive lemma.
There are two possible places to refine a lemma template: on its antecedent (line 19) and its
consequent (line 20). We aim to synthesize a lemma which has an as weak as possible antecedent
or an as strong as possible consequent. We will elaborate the details in Subsections 5.3 and 5.4.
Our framework immediately returns a non-empty set of synthesized lemmas (lines 21) once it
successfully refines a template. Otherwise, it returns an empty set (∅) indicating that no lemma
can be synthesized (line 22).
5.2

Discovering lemma templates

The lemma templates for a given goal entailment can be discovered from the entailment’s heap
structure. In the followings, we present the formal definition of the lemma templates and also
illustrate by examples how to create them.
Definition 5.1 (Lemma template). A lemma template for a goal entailment F 1 |− F 2 is an entailment
of the form Σ1 |− ∃v.Σ
® 2 , where:
(1) Σ1 and Σ2 are spatial formulas containing at least one inductive heap predicate.
(2) Heap predicate symbols in Σ1 and Σ2 are sub-multisets of those in F 1 and F 2 .
(3) Variables in Σ1 and Σ2 are separately named (no variables appear twice) and v® ≡ FV(Σ2 ).
The condition (1) limits the templates for only inductive lemmas. The condition (2) guarantees that
the synthesized lemmas are unifiable with the goal entailment via applications of the rules LML
and LMR . Moreover, the condition (3) ensures that each template is as general as possible so that
desirable pure constraints can be subsequently discovered in the next phases.
For instance, the following lemma templates can be created given the motivating entailment in
Section 2: E 1 ≜ dllrev(x, y, u, v, n) ∗ dll(v, u, z, t, 200) ∧ n≥100 |− ∃r .(dll(x, y, r , z, n+199) ∗ z7→r, t).
Note that the template T1 is used to synthesize the lemma L 1 ≜ dllrev(a, b, c, d, m) |− dll(a, b, c, d, m).
T1 ≜ dllrev(x 1 , x 2 , x 3 , x 4 , n 1 ) |− ∃x 5 , x 6 , x 7 , x 8 , n 2 .dll(x 5 , x 6 , x 7 , x 8 , n 2 )
dll(x 1 , x 2 , x 3 , x 4 , n 1 ) |− ∃x 5 , x 6 , x 7 , x 8 , x 9 , x 10 , x 11 , n 2 .(dll(x 5 , x 6 , x 7 , x 8 , n 2 ) ∗ x 9 7→x 10 , x 11 )
dllrev(x 1 , x 2 , x 3 , x 4 , n 1 ) |− ∃x 5 , x 6 , x 7 , x 8 , x 9 , x 10 , x 11 , n 2 .(dll(x 5 , x 6 , x 7 , x 8 , n 2 ) ∗ x 9 7→x 10 , x 11 )
dllrev(x 1 , x 2 , x 3 , x 4 , n 1 ) ∗ dll(x 5 , x 6 , x 7 , x 8 , n 2 ) |− ∃x 9 , x 10 , x 11 , x 12 , n 3 .dll(x 9 , x 10 , x 11 , x 12 , n 3 )
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:17

Similarly, there can be several possible lemma templates relating to the entailments E 2 and E 3 in
Figure 1. Among them, the templates T2 and T3 below are used to synthesize the lemmas L 2 and L 3 :
T2 ≜ dll(x 1 , x 2 , x 3 , x 4 , n 1 ) ∗ dll(x 5 , x 6 , x 7 , x 8 , n 2 ) |− ∃x 9 , x 10 , x 11 , x 12 , n 3 .dll(x 9 , x 10 , x 11 , x 12 , n 3 )
T3 ≜ dll(x 1 , x 2 , x 3 , x 4 , n 1 ) |− ∃x 5 , x 6 , x 7 , x 8 , x 9 , x 10 , x 11 , n 2 .(dll(x 5 , x 6 , x 7 , x 8 , n 2 ) ∗ x 9 7→x 10 , x 11 )

5.3

Refining the lemma template’s antecedent

Figure 12 presents the antecedent refinement procedure (RefineAnte), which aims to strengthen
the antecedent of a lemma template Σ1 ∧ Π 1 |− Σ2 with pure constraints of all its variables. Note
that when RefineAnte is invoked in the first time by SynthesizeLemma (Figure 11, line 19), Π 1 is
set to true and the existential quantification ∃v® in the original template Σ1 |− ∃v.Σ
® 2 is removed
since the antecedent will be strengthened with constraints of all variables in the template.
Initially, RefineAnte creates an unProcedure RefineAnte(L, Σ1 ∧ Π 1 |− Σ2 )
known entailment Σ1 ∧Π 1 ∧U (®
u) |− Σ2 ,
Input: Σ1 ∧Π1 |−Σ2 is a lemma template, L is a valid lemma set
where U (®
u) is an unknown relation
Output: a set of at most one synthesized lemma
of all variables u® in Σ1 , Σ2 , Π 1 (lines
Requires: valid(L)
23, 24). Then, it proves the entailment
Ensures: (res = ∅) ∨ ∃ Π 1′ .(res = {Σ1 ∧Π 1 ∧Π 1′ |−Σ2 } ∧ valid(res))
by induction and collects a set A of
23: u® ← FreeVars(Σ1 , Σ2 , Π 1 )
unknown assumptions, if any, about
24: U (®
u) ← CreateUnknownRelation(®
u)
U (®
u) (line 25). In this proof deriva- 25: r, _, A ← Prove(∅, L, Σ ∧ Π ∧ U (®
u) |− Σ2 , NoSyn)
1
1
tion (also in other invocations of Prove 26: if r = Valid⟨_⟩ then
in the lemma synthesis), we prevent 27: for each A ′ in SuperSet(A) do
the proof system from synthesizing 28:
U (®
u) ← Solve(A ′, U (®
u))
new lemmas (by passing NoSyn) to 29:
if Σ1 ∧ Π 1 ∧ U (®
u) . false then
avoid initiating a new lemma synthe- 30:
u) |− Σ2 )
L ← (Σ1 ∧ Π 1 ∧ U (®
r ′, _, _ ← Prove(∅, L, L, NoSyn)
//Verify ...
sis phase inside the current synthesis, 31:
if r ′ = Valid⟨ξ ⟩ and IH ∈ ξ then
//and return ...
i.e., to prohibit the nested lemma syn- 32:
return {L}
//the first inductive lemma,
thesis. In addition, the assumption set 33:
34:
else
return
RefineAnte(L,
L) //or continue refining.
A will be examined, via the procedure
35:
return
∅
//No lemmas are found.
Solve, to discover a solution of U (®
u)
(lines 27, 28). We implement in Solve
Fig. 12. Refining a lemma template’s antecedent
a constraint solving technique using
Farkas’ lemma [Colón et al. 2003; Schrijver 1986]. This technique assigns U (®
u) to a predefined linear
arithmetic formula with unknown coefficients, and applies Farkas’ lemma to transform A into a
set of constraints involving only the unknown coefficients. Then, it utilizes an off-the-shelf prover
such as Z3 [Moura and Bjørner 2008] to find a concrete model of the coefficients, thus obtains the
actual definition U (®
u) of U (®
u). We will describe this technique in Subsection 5.6.
Furthermore, we aim to find a non-spurious solution U (®
u) which does not refute the antecedent,
i.e., Σ1 ∧ Π 1 ∧ U (®
u) . false, to avoid creating an useless lemma: false |− Σ2 (line 29). To examine
this refutation, we follow the literature [Brotherston et al. 2014; Le et al. 2016] to implement an
unsatisfiability checking algorithm, which over-approximates a symbolic-heap formula to a pure
formula and invokes the off-the-shelf prover (such as Z3) to check the pure formula’s unsatisfiability,
thus concludes about the unsatisfiability of the original formula.
In general, discovering a non-spurious solution U (®
u) is challenging, because:
– The assumption set A can be complicated since the parameters u® of the unknown relation U (®
u)
are all variables in the lemma template. This complexity can easily overwhelm the underlying
prover when finding the model of the corresponding unknown coefficients.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:18

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

– The discovered proof tree of the unknown entailment might not be similar to the actual proof
tree of the desired lemma, due to the occurrence of the unknown relation. Therefore, the set A
might contain noise assumptions of U (®
u), which results in a spurious solution. Nonetheless, a
part of the expected solution can still be discovered from a subset of A, which corresponds to
the common part of the discovered and the desired proof trees.
The above challenges inspire us to design an exhaustive approach to solve A (line 27). In particular,
RefineAnte first solves the entire set A (the first element in SuperSet(A)) to find a complete
solution, which satisfies all assumptions in A. If such solution is not available, RefineAnte iteratively
examines each subset of A (among the remaining elements in SuperSet(A)) to discover a partial
solution, which satisfies some assumptions in A.
The discovered solution (complete or partial) will be verified whether it can form a valid inductive
lemma. In particular, the proof system will be invoked to prove the candidate lemma L (line 31). The
verification is successful when L is proved valid and its witness proof tree ξ contains an induction
hypothesis application (labeled by IH) (line 32). The latter condition ensures that the returned
lemma is actually an inductive lemma.
We also follow an incremental approach to refine the lemma template’s antecedent. That is, the
antecedent will be strengthened with the discovered solution U (®
u) to derive a new template. The
new template will be refined again until the first valid lemma is discovered (lines 32 – 34). Note
that this refinement stops at the first solution to ensure that the discovered antecedent is as weak
as possible. Finally, RefineAnte returns ∅ if no valid inductive lemma can be discovered (line 35).
For example, given the template T1 ≜ dllrev(x 1 , x 2 , x 3 , x 4 , n 1 ) |− ∃x 5 , x 6 , x 7 , x 8 , n 2 .dll(x 5 , x 6 , x 7 , x 8 , n 2 ),
RefineAnte creates an unknown relation U (x 1 , ..., x 8 , n 1 , n 2 ) and introduces the entailment Eu1 :
Eu1 ≜ dllrev(x 1 , x 2 , x 3 , x 4 , n 1 ) ∧ U (x 1 , ..., x 8 , n 1 , n 2 ) |− dll(x 5 , x 6 , x 7 , x 8 , n 2 )
x, n)
® →
A1 ≜ {x 1 =x 3 ∧ n 1 =1 ∧ U (®
A2 ≜ {U (®
x, n)
® → false}
x 1 =x 5 ∧x 2 =x 6 ∧x 4 =x 8 ∧x 5 =x 7 ∧n 2 =1} 1
UΠ
U1Σ
x 1 =x 3 ∧ n 1 =1 ∧ U (®
x, n)
® |− x 1 =x 5 ∧
x 3 7→u, x 4 ∧ U (®
x, n)
® |− a 5 =x 5 ∧
x 2 =x 6 ∧ x 4 =x 8 ∧ x 5 =x 7 ∧ n 2 =1
a 6 =x 6 ∧ a 7 =x 7 ∧ a 8 =x 8 ∧ b2 =n 2
∗7→
∗P
dll(a 5 , a 6 , a 7 , a 8 , b2 ) ∗ x 3 7→u, x 4 ∧
x 1 7→x 2 , x 4 ∧ x 1 =x 3 ∧ n 1 =1 ∧ U (®
x, n)
®
® }
A3 ≜ {U (®
x, n)
® → U (®
a, b)θ
|− x 5 7→x 6 , x 8 ∧ x 5 =x 7 ∧ n 2 =1
U (®
x, n)
® |− dll(x 5 , x 6 , x 7 , x 8 , n 2 )
PR
UIH
x 1 7→x 2 , x 4 ∧ x 1 =x 3 ∧ n 1 =1 ∧ U (®
dllrev(x 1 , x 2 , u, x 3 , n 1 −1) ∗ x 3 7→u, x 4 ∧ U (®
x, n)
®
x, n)
®
|− dll(x 5 , x 6 , x 7 , x 8 , n 2 )
|− dll(x 5 , x 6 , x 7 , x 8 , n 2 )
ID

Eu1 ≜ dllrev(x 1 , x 2 , x 3 , x 4 , n 1 ) ∧ U (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 , n 1 , n 2 ) |− dll(x 5 , x 6 , x 7 , x 8 , n 2 )
Fig. 13. A possible proof tree of the unknown entailment Eu1
® ≡ U (a 1 , a 2 , a 3 , a 4 , a 5 , a 6 , a 7 , a 8 , b1 , b2 );
where U (®
x, n)
® ≡ U (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 , n 1 , n 2 ); U (®
a, b)
® |− dll(a 5 , a 6 , a 7 , a 8 , b2 );
the rule ID is performed to record the IH H ≜ dllrev(a 1 , a 2 , a 3 , a 4 , b1 ) ∧ U (®
a, b)
the rule UIH applies H with θ = [x 1 /a 1 , x 2 /a 2 , u/a 3 , x 3 /a 4 , n 1 −1/b1 ];

Figure 13 presents a possible proof tree of Eu1 . From this proof, we obtain a set A = A1 ∪ A2 ∪ A3
of three unknown assumptions about the relation U (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 , n 1 , n 2 ):
(1) x 1 =x 3 ∧ n 1 =1 ∧ U (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 , n 1 , n 2 ) → x 1 =x 5 ∧ x 2 =x 6 ∧ x 4 =x 8 ∧ x 5 =x 7 ∧ n 2 =1
(2) U (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 , n 1 , n 2 ) → false
(3) U (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 , n 1 , n 2 ) → U (x 1 , x 2 , u, x 3 , a 5 , a 6 , a 7 , a 8 , n 1 −1, b2 )

Our framework first attempts to solve the full assumption set A. Unfortunately, there is only a
spurious solution U (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 , n 1 , n 2 ) ≡ false, since the assumption (2) is too strong.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:19

It then tries to find another solution by partially solving the set A. In this case, it can discover the
following partial solution U when solving a subset containing only the assumption (1):
U (x 1 , x 2 , x 3 , x 4 , x 5 , x 6 , x 7 , x 8 , n 1 , n 2 ) ≡ x 1 =x 5 ∧ x 2 =x 6 ∧ x 3 =x 7 ∧ x 4 =x 8 ∧ n 1 =n 2

Since the above is only a partial solution, the framework needs to verify whether it can construct
a valid inductive lemma. Indeed, U can be used to derive the following entailment Eu1 , which can
be simplified to become dllrev(x 1 , x 2 , x 3 , x 4 , n 1 ) |− dll(x 1 , x 2 , x 3 , x 4 , n 1 ). The latter entailment can be
equivalently transformed into the motivating lemma L 1 by a renaming on its variables.
Eu1 ≜ dllrev(x 1 , x 2 , x 3 , x 4 , n 1 ) ∧ x 1 =x 5 ∧ x 2 =x 6 ∧ x 3 =x 7 ∧ x 4 =x 8 ∧ n 1 =n 2 |− dll(x 5 , x 6 , x 7 , x 8 , n 2 )

5.4

Refining the lemma template’s consequent

The consequent refinement is presented in the procedure RefineConseq (Figure 14). Unlike the
antecedent refinement, this refinement is not straightforward by simply adding pure constraints
into the template’s consequent, since the existing template’s antecedent might not be strong enough
to prove any formulas derived from the consequent. For example, all entailments derived from
adding pure constraints to only the consequent of the lemma template T3 are invalid, because when
n 1 =1, the list dll(x 1 , x 2 , x 3 , x 4 , n 1 ) has the length of 1, thus cannot be split into a singleton heap
x 9 7→x 10 , x 11 and a list dll(x 5 , x 6 , x 7 , x 8 , n 2 ), whose length is at least 1, by the definition of dll.
T3 ≜ dll(x 1 , x 2 , x 3 , x 4 , n 1 ) |− ∃x 5 , x 6 , x 7 , x 8 , x 9 , x 10 , x 11 , n 2 .(dll(x 5 , x 6 , x 7 , x 8 , n 2 ) ∗ x 9 7→x 10 , x 11 )

To overcome this problem,
|
® 2)
we decompose the consequent Procedure RefineConseq(L, Σ1 − ∃v.Σ
|
® 2 is a lemma template, L is a set of valid lemmas
refinement into two phases, Input: Σ1 − ∃v.Σ
preprocessing and fine-tuning. Output: a set of at most one synthesized lemma
For an input lemma template Requires: valid(L)
|− ® 2 ∧Π 2 )} ∧ valid(res))
Σ1 |− ∃v.Σ
® 2 , in the first phase, Ensures: (res = ∅) ∨ ∃ Π1 ,Π2 .(res = {Σ1 ∧Π1 ∃v.(Σ
36: T ← Preprocess(L, Σ1 |− ∃v.Σ
®
)
2
the framework infers a pure
37: if T = {Σ1 ∧ Π 1 |− ∃v.Σ
® 2 } then
constraint Π 1 so that the entail® 2 ∧ true))
38:
return FineTuneConseq(L, Σ1 ∧ Π1 |− ∃v.(Σ
ment Σ1 ∧ Π 1 |− ∃v.Σ
® 2 is valid
39: return ∅
(lines 36, 37). In the second phase, it incrementally
Fig. 14. Refining a lemma template’s consequent
strengthens the consequent of
the derived entailment until discovers a valid inductive lemma (line 38). Note that, we retain the
existential quantification in this consequent, and any constraints added into the consequent will be
bound by this quantification. These two phases will be elaborated in details as follows.
Preprocessing a lemma template.
Figure 15 presents our antecedent preprocessing procedure (Preprocess). Similar to the antecedent
refinement in Section 5.3, this procedure strengthens the antecedent of the template Σ1 |− ∃v.Σ
® 2
with a non-spurious condition Π 1 to make the lemma template valid. We also prevent the framework
from entering nested lemma synthesis phases by invoking Prove in the NoSyn mode (line 43).
However, this preprocessing step differs from the antecedent refinement (Section 5.3) when it
creates an unknown entailment by introducing the unknown relation U (®
u) on only the antecedent’s
free variables u® (lines 40, 41). We also equip the consequent ∃v.Σ
® 2 of the unknown entailment
with a conjunction Πinv of its inductive heap predicates’ pure invariants (lines 42, 43). These
invariants are pure formulas representing Boolean constraints of the predicates’ variables. We will
briefly describe the invariant construction in Section 5.5. This construction is also well-studied in
separation logic literature [Brotherston et al. 2014; Chin et al. 2012; Le et al. 2016].
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:20

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

In theory, equipping additional pure invariants of inductive heap predicates
does not weaken or strengthen the
lemma template’s consequent, i.e., Σ2 ≡
Σ2 ∧ Πinv . In our approach, Preprocess
solves the entire assumption constraint
set A at once (line 45), and not incrementally as in the antecedent refinement (Section 5.3). Therefore, the additional pure invariant Πinv is useful
for Preprocess to solve the entire set A
more precisely and effectively.

Procedure Preprocess(L, Σ1 |− ∃v.Σ
® 2)
® 2 is a lemma template, L is a valid lemma set
Input: Σ1 |−∃v.Σ
Output: a set of at most one refined template

Requires: valid(L)
Ensures: (res = ∅) ∨ ∃ Π1 .(res = {Σ1 ∧Π 1 |−∃v.Σ
® 2 } ∧ valid(res))
40: u® ← FreeVars(Σ1 )
41: U (®
u) ← CreateUnknownRelation(®
u)
Ó
42: Πinv ←
x))
P(x® ) ∈ Σ2 Invariant(P(®
43: r , _, A ← Prove(∅, L, Σ1 ∧U (®
u) |−∃v.(Σ
® 2 ∧Πinv ), NoSyn)
44: if r = Valid⟨_⟩ then
45:
U (®
u) ← Solve(A, U (®
u))
u) . false then return {Σ1 ∧ U (®
u) |− ∃v.Σ
® 2}
46:
if Σ1 ∧ U (®
//No refined templates are found.
For example, given the template T3 , 47: return ∅

Preprocess sets up an unknown reFig. 15. Preprocess a lemma template’s antecedent
lation U (x 1 , x 2 , x 3 , x 4 , n 1 ) in the template’s antecedent, and introduces the invariant n 2 ≥1 of dll(x 5 , x 6 , x 7 , x 8 , n 2 ) in the template’s
consequent to create the following unknown entailment Eu2 .
Eu2 ≜ dll(x 1 , x 2 , x 3 , x 4 , n 1 ) ∧ U (x 1 , x 2 , x 3 , x 4 , n 1 ) |− ∃x 5, ...,11 , n 2 .(dll(x 5 , x 6 , x 7 , x 8 , n 2 ) ∗ x 9 7→x 10 , x 11 ∧ n 2 ≥1)
A2 ≜ {U (x 1, 2, 3, 4, n 1 ) → ∃x 5, . . ., 11, n 2 .(x 1 =x 9 ∧ x 2 =x 10 ∧
u=x 11 ∧ u=x 5 ∧ x 1 =x 6 ∧ x 3 =x 7 ∧ x 4 =x 8 ∧ n 1 −1=n 2 ∧ n 2 ≥1)} 1
UΠ
U2Σ U (x
1, 2, 3, 4, n 1 ) |− ∃x 5, . . ., 11, n 2 .(x 1 =x 9 ∧ x 2 =x 10 ∧
x 1 =x 3 ∧ n 1 =1 ∧ U (x 1, 2, 3, 4, n 1 ) |−
u=x 11 ∧ u=x 5 ∧ x 1 =x 6 ∧ x 3 =x 7 ∧ x 4 =x 8 ∧ n 1 −1=n 2 ∧ n 2 ≥1)
∃x 5, . . ., 11, n 2 .(dll(x 5, x 6, x 7, x 8, n 2 ) ∧
∗P
dll(u, x 1, x 3, x 4, n 1 −1) ∧ U (x 1, 2, 3, 4, n 1 ) |− ∃x 5, . . ., 11, n 2 .
x 1 =x 9 ∧ x 2 =x 10 ∧ x 4 =x 11 ∧ n 2 ≥1)
∗7→
(dll(x 5, x 6, x 7, x 8, n 2 ) ∧ x 1 =x 9 ∧ x 2 =x 10 ∧ u=x 11 ∧ n 2 ≥1)
x 1 7→x 2, x 4 ∧ x 1 =x 3 ∧ n 1 =1 ∧ U (x 1, 2, 3, 4, n 1 ) |−
∗7→
x 1 7→x 2, u ∗ dll(u, x 1, x 3, x 4, n 1 −1) ∧ U (x 1, 2, 3, 4, n 1 ) |−
∃x 5, . . ., 11, n 2 .(dll(x 5, x 6, x 7, x 8, n 2 ) ∗
∃x 5, . . ., 11, n 2 .(dll(x 5, x 6, x 7, x 8, n 2 ) ∗ x 9 7→x 10, x 11 ∧ n 2 ≥1)
x 9 7→x 10, x 11 ∧ n 2 ≥1)
ID
Eu2 ≜ dll(x 1, x 2, x 3, x 4, n 1 ) ∧ U (x 1, x 2, x 3, x 4, n 1 ) |− ∃x 5, . . ., 11, n 2 .(dll(x 5, x 6, x 7, x 8, n 2 ) ∗ x 9 7→x 10, x 11 ∧ n 2 ≥1)

A1 ≜ {x 1 =x 3 ∧ n 1 =1 ∧ U (x 1, 2, 3, 4, n 1 ) → false }

Fig. 16. A possible proof tree of the unknown entailment Eu2

This entailment will be proved by induction to collect constraints about the unknown relation U . We
present its detailed proof in Figure 16. Observe that the assumption constraint U (x 1 , x 2 , x 3 , x 4 , n 1 ) →
∃x 5 , . . . , x 11 , n 2 .(x 1 =x 9 ∧x 2 =x 10 ∧u=x 11 ∧u=x 5 ∧x 1 =x 6 ∧x 3 =x 7 ∧x 4 =x 8 ∧n 1 −1=n 2 ∧n 2 ≥1) in A2 can
be simplified by eliminating existentially quantified variables to become U (x 1 , x 2 , x 3 , x 4 , n 1 ) → n 1 ≥2.
Therefore, we can obtain a set A = A1 ∪ A2 containing the following unknown assumptions:
(1) x 1 =x 3 ∧ n 1 =1 ∧ U (x 1 , x 2 , x 3 , x 4 , n 1 ) → false

(2) U (x 1 , x 2 , x 3 , x 4 , n 1 ) → n 1 ≥2

The procedure Preprocess can solve the full assumption constraint set A to discover a potential
solution U (x 1 , x 2 , x 3 , x 4 , n 1 ) ≡ n 1 ≥2, which allows T3 to be refined to a new lemma template T3′:
T3′ ≜ dll(x 1 , x 2 , x 3 , x 4 , n 1 ) ∧ n 1 ≥2 |− ∃x 5 , . . . , x 11 , n 2 .(dll(x 5 , x 6 , x 7 , x 8 , n 2 ) ∗ x 9 7→x 10 , x 11 )

Fine-tuning a lemma template’s consequent.
This step aims to refine further the consequent of the lemma template discovered in the preprocessing phase. The refinement is performed by the recursive procedure FineTuneConseq (Figure 17).
Its input is a (refined) lemma template Σ1 ∧ Π 1 |− ∃v.(Σ
® 2 ∧ Π 2 ). When FineTuneConseq is invoked
in the first time by RefineConseq, Π 2 is set to true (Figure 14, line 38).
Initially, FineTuneConseq establishes an unknown relation U (®
u) on all variables in the templates
and creates an unknown entailment Σ1 ∧ Π 1 |− ∃v.(Σ
® 2 ∧ Π 2 ∧ U (®
u)) (lines 48, 49). Then, it proves the
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:21

unknown entailment by induction to collect a set A of unknown assumptions (line 50). Similarly to
the antecedent refinement (Section 5.3), A will be exhaustively solved: the entire set and its subsets
will be examined until a feasible solution is found to obtain a valid inductive lemma (lines 52 – 59).
We also prevent the proof
system from entering nested
lemma synthesis phases, controlled by the argument NoSyn,
when Prove is invoked to collect the unknown assumption
set A (line 50) or to verify
the inductive lemma (line 55).
Witness proof tree of a candidate lemma, if having, is examined for the occurrence of the
induction hypothesis application rule (IH), to determine if
this candidate is a valid inductive lemma (line 56).

Procedure FineTuneConseq(L, Σ1 ∧ Π1 |− ∃v.(Σ
® 2 ∧ Π 2 ))
® 2 ∧Π 2 ) is a lemma template, L is a valid lemma set
Input: Σ1 ∧Π 1 |−∃v.(Σ
Output: a set of at most one synthesized lemma
Requires: valid(L)
Ensures: (res = ∅) ∨ ∃ Π2′ .(res = {Σ1 ∧Π 1 |−∃v.(Σ
® 2 ∧Π 2 ∧Π2′ )} ∧ valid(res))
48: u® ← FreeVars(Σ1 , Σ2 , Π 1 , Π 2 )
49: U (®
u) ← CreateUnknownRelation(®
u)
® 2 ∧ Π 2 ∧U (®
u)), NoSyn)
50: r , _, A ← Prove(∅, L, Σ1 ∧ Π 1 |− ∃v.(Σ
51: if r = Valid⟨_⟩ then
52:
for each A ′ in SuperSet(A) do
U (®
u) ← Solve(A ′, U (®
u))
53:
54:
L ← (Σ1 ∧ Π1 |− ∃v.(Σ
® 2 ∧ Π 2 ∧ U (®
u))
55:
r ′, _, _ ← Prove(∅, L, L, NoSyn)
//Verify ...
56:
if r ′ = Valid⟨ξ ⟩ and IH ∈ ξ then //the inductive lemma, and ...
57:
Lsyn ← FineTuneConseq(L, L) //strengthen its consequent.
58:
if Lsyn = ∅ then return {L}
However, unlike the antecedent 59:
else return Lsyn

refinement, FineTuneConseq 60: return ∅
//No lemmas are found.
keeps refining the template
until its consequent cannot be
Fig. 17. Fine-tuning the consequent of a lemma template
refined further (line 56, 59).
This repetition ensures that the returned lemma’s consequent, if discovered, is as strong as possible.
For example, given the preprocessed template T3′, FineTuneConseq creates an unknown relation
U (x 1 , . . . , x 11 , n 1 , n 2 ), or U (®
x, n)
® for short, involving all variables in T3′ and constructs the unknown
entailment Eu3 . This entailment will be proved again to collect constraints about U (®
x, n).
®
x, n))
®
Eu3 ≜ dll(x 1 , x 2 , x 3 , x 4 , n 1 ) ∧ n 1 ≥2 |− ∃x 5 , . . . , x 11 , n 2 .(dll(x 5 , x 6 , x 7 , x 8 , n 2 ) ∗ x 9 7→x 10 , x 11 ∧ U (®
A3 ≜ {n 1≥2 ∧ r =x 3 ∧ n 1 −2=1 → ∃x 5, . . ., 11,n 2,v .(U (x,
® n)
® ∧ x 1 =x 5 ∧
x 2 =x 6 ∧ u=v ∧ v=x 7 ∧ r =x 8 ∧ r =x 9 ∧ u=x 10 ∧ x 4 =x 11 ∧ n 2 −1=1)}
n 1 ≥2 ∧ r =x 3 ∧ n 1 −2=1 |− ∃x 5, . . ., 11,n 2,v .(U (x,
® n)
® ∧ x 1 =x 5 ∧
x 2 =x 6 ∧ u=v ∧ v=x 7 ∧ r =x 8 ∧ r =x 9 ∧ u=x 10 ∧ x 4 =x 11 ∧ n 2 −1=1)
r 7→u,x 4 ∧ n 1 ≥2 ∧ r =x 3 ∧ n 1 −2=1 |− ∃x 5, . . ., 11,n 2,v .(x 9 7→x 10,x 11 ∧
U (x,
® n)
® ∧ x 1 =x 5 ∧ x 2 =x 6 ∧ u=v ∧ v=x 7 ∧ r =x 8 ∧ n 2 −1=1)

A1
...

U1Π
A4

∗7→
...

A2

dll(r,u,x 3,x 4,n 1 −2) ∧ n 1 ≥2 |− ∃x 5, . . ., 11,n 2,v .(x 9 7→x 10,x 11 ∧
U (x,
® n)
® ∧ x 1 =x 5 ∧ x 2 =x 6 ∧ u=v ∧ v=x 7 ∧ r =x 8 ∧ n 2 −1=1)

...

u7→x 1,r ∗dll(r,u,x 3,x 4,n 1 −2) ∧ n 1 ≥2 |− ∃x 5, . . ., 11,n 2,v .(v7→x 5,x 8 ∗
x 9 7→x 10,x 11 ∧ U (x,
® n)
® ∧ x 1 =x 5 ∧ x 2 =x 6 ∧ u=v ∧ v=x 7 ∧ n 2 −1=1)

ID
∗7→

dll(u,x 1,x 3,x 4,n 1 −1)∧n 1≥2 |−∃x 5, . . ., 11,n 2,v .(v7→x 5,x 8 ∗x 9 7→x 10,x 11 ∧U (x,
® n)∧x
®
1 =x 5 ∧x 2 =x 6 ∧u=v∧v=x 7 ∧n 2 −1=1)

ID

dll(u,x 1,x 3,x 4,n 1 −1)∧n 1≥2 |−∃x 5, . . ., 11,n 2,v .(dll(v,x 5,x 7,x 8,n 2 −1)∗x 9 7→x 10,x 11 ∧U (x,
® n)∧x
®
1 =x 5 ∧x 2 =x 6 ∧u=v)

PR

x 1 7→x 2,u ∗ dll(u,x 1,x 3,x 4,n 1 −1)∧n 1≥2 |−∃x 5, . . ., 11,n 2,v .(x 5 7→x 6,v∗dll(v,x 5,x 7,x 8,n 2 −1)∗x 9 7→x 10,x 11 ∧U (x,
® n))
®

∗7→
PR

x 1 7→x 2,u ∗ dll(u,x 1,x 3,x 4,n 1 −1)∧n 1≥2 |−∃x 5, . . ., 11,n 2 .(dll(x 5,x 6,x 7,x 8,n 2 )∗x 9 7→x 10,x 11 ∧U (x,
® n))
®
ID
Eu3 ≜ dll(x 1,x 2,x 3,x 4,n 1 ) ∧ n 1≥2 |− ∃x 5, . . ., 11,n 2 .(dll(x 5,x 6,x 7,x 8,n 2 ) ∗ x 9 7→x 10,x 11 ∧ U (x,
® n))
®

Fig. 18. A partial proof tree of the unknown entailment Eu3

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:22

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

We present a partial proof tree of Eu3 in Figure 18, where FineTuneConseq is able to collect a set of
unknown assumptions A = A1 ∪ A2 ∪ A3 ∪ A4 . More specifically, A3 ≜ {n 1 ≥2 ∧r =x 3 ∧n 1 −2=1 |−
∃x 5, ...,11 , n 2 , v. (U (®
x, n)
® ∧ x 1 =x 5 ∧ x 2 =x 6 ∧u=v ∧v=x 7 ∧ r =x 8 ∧ r =x 9 ∧u=x 10 ∧ x 4 =x 11 ∧ n 2 −1=1)} is
an assumption subset derived from a potential proof path of an inductive lemma, and A1 , A2 , A4
relate to other proof paths. The set A can be partially solved by considering only A3 . Here, a
possible solution of A3 is U p (x 1 , ..., x 11 , n 1 , n 2 ) ≡ x 1 =x 5 ∧ x 2 =x 6 ∧ x 3 =x 8 ∧ x 4 =x 11 ∧ x 7 =x 10 ∧ x 8 =x 9 .
This solution can be substituted back to Eu3 to derive the refined lemma template T3′′.
T3′′ ≜ dll(x 1 , x 2 , x 3 , x 4 , n 1 ) ∧ n 1 ≥2 |− ∃x 7 , n 2 .(dll(x 1 , x 2 , x 7 , x 3 , n 2 ) ∗ x 3 7→x 7 , x 4 )

Then, FineTuneConseq constructs another unknown entailment U ′(x 1 , x 2 , x 3 , x 4 , x 7 , n 1 , n 2 ) on all
variables of T3′′ and creates a new unknown entailment, which will be proved again to find a solution
′
U p (x 1 , x 2 , x 3 , x 4 , x 7 , n 1 , n 2 ) ≡ n 1 =n 2 +1. This solution helps to refine the template T3′′ to obtain an
inductive lemmaT 3 ≜ dll(x 1 , x 2 , x 3 , x 4 , n 1 )∧n 1 ≥2 |− ∃x 7 .(dll(x 1 , x 2 , x 7 , x 3 , n 1 −1)∗x 3 7→x 7 , x 4 ), which
can be equivalently transformed to the motivating lemma L 3 in Section 2.
5.5

Inferring pure invariants of inductive heap predicates

We present in this subsection the construction of inductive heap predicates’ invariants, which are
mainly utilized to preprocess the lemma templates’ antecedents (Section 5.4). Our construction is
inspired from separation logic literature [Brotherston et al. 2014; Chin et al. 2012; Le et al. 2016].
Definition 5.2 (Invariant of inductive heap predicates). Given an inductive heap predicate P(®
x), a pure
formula Invariant(P(®
x)) is called an invariant of P(®
x) iff s, h |= P(®
x) implies that s |= Invariant(P(®
x)),
for all model s, h. Formally, ∀s, h. (s, h |= P(®
x) → s |= Invariant(P(®
x))).
Constructing pure invariants. We also exploit a template-based approach to discover the pure
invariants. For a system of k (mutually) inductive heap predicates P1 (®
x 1 ), . . . , Pk (®
x k ), we first create
k unknown relations UP1 (®
x 1 ), . . . , UPk (®
x k ) to respectively represent their desired invariants. Then,
we follow the predicates’ definitions to establish constraints about the unknown relations.
In particular, consider each definition case F ji (x®i ) of a predicate Pi (®
x i ), which is of the form
u 1 ), ..., Qn (®
un ) are all inductive heap predicates in Σij ,
F ji (x®i ) ≜ ∃®
u.(Σij ∧ Πij ). Suppose that Q1 (®
where Q1 , ..., Qn ∈ {P1 , ..., Pk }, we create the following unknown assumption:
UQ1 (®
u 1 ) ∧ . . . ∧ UQn (®
un ) ∧ Πij

→

UPi (®
xi )

Thereafter, the system of all unknown assumptions can be solved by the constraint solving technique
based on Farkas’ lemma (Section 5.6) to discover the actual invariants of P1 (x®1 ), . . . , Pk (x®k ).
For example, given the predicate dll(hd, pr, tl, nt, len) in Section 2, whose definition is
dll(hd, pr , tl, nt, len)

=

def

(hd7→pr , nt ∧ hd=tl ∧ len=1) ∨ ∃u.(hd7→pr , u ∗ dll(u, hd, tl, nt, len−1))

We create an unknown relation Udll (hd, pr, tl, nt, len) representing its invariant and follow the
definition of dll(hd, pr, tl, nt, len) to establish the following constraints:
(1) hd=tl ∧ len=1 → Udll (hd, pr , tl, nt, len)

(2) Udll (u, hd, tl, nt, len−1) → Udll (hd, pr, tl, nt, len)

We then solve these constraints to obtain the solution U dll (hd, pr, tl, nt, len) ≡ len ≥ 1, which is
also the invariant of dll(hd, pr, tl, nt, len).
5.6

Solving assumption constraints with Farkas’ lemma

In this subsection, we describe the underlying constraint solving technique based on Farkas’ lemma.
This technique is implemented in the procedure Solve, which is frequently invoked in the lemma
synthesis to solve an unknown assumption set (Sections 5.3, 5.4, and 5.5). We will formally restate
Farkas’ lemma and explain how it is applied in constraint solving.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:23

Ó Ín
Farkas’ lemma [Schrijver 1986]. Given a conjunction of linear constraints m
j=1 i=1a i j x i + b j ≥ 0,
Í
which is satisfiable, and a linear constraint ni=1c i x i + γ ≥ 0, we have:
n
n
m
m
m Í
n


Í
Í
Í
Ó
Ó
∀x 1 . . . x n .

ai j x i + b j ≥ 0 →

j=1 i=1

ci xi + γ ≥ 0

iff

i=1

∃λ 1 . . . λm ≥ 0.

ci =

i=1

λ j ai j ∧

j=1

λj bj ≤ γ

j=1

Solving constraints. Given an assumption set A of an unknown relation U (x 1 , . . . , xm , u 1 , . . . , un ),
where x 1 , . . . , xm are spatial variables and u 1 , . . . , un are integer variables, the procedure Solve
aims to find an actual definition U of U in the following template, where c i j , di j are unknown
coefficients, M, N are pre-specified numbers of conjuncts.


ÓM Ím
ÓN Ín
U (x 1 , . . . , xm , u 1 , . . . , un )

≜

j=1

i=1c i j x i

+ c 0j ≥ 0 ∧

j=1

i=1di j ui

+ d 0j ≥ 0

Recall that our lemma synthesis framework can incrementally discover the final solution U in
several passes. Hence, we can set M, N small, e.g., 1≤M,N ≤3, or M=0, N ≤6 (no spatial contraints), or
M ≤6, N =0 (no arithmetic constraints) to make the constraint solving more effective. We restrict the
coefficients c i j to represent equality or disequality constraints of spatial variables, e.g., x k =xl , x k ,xl ,
x k =0, and x k ,0, where 0 denotes nil. The constraint x k =xl can be encoded as x k −xl ≥0 ∧ −x k +xl ≥0,
or the encoding of x k ,xl is x k −xl −1≥0. Therefore, it requires that −1≤c i j ≤1 forÍ
i>0, and c 0j =0
(forÍequalities) or c 0j =−1 (for disequalities). We also add the restrictions −1 ≤ m
i=1c i j ≤ 1 and
1≤ m
|c
|
≤
2
to
ensure
that
the
spatial
constraints
involve
at
most
two
variables.
i=1 i j
In summary, the assumption set A of the unknown relation U can be solved in three steps:
– Normalize assumptions in the set A into the form of Horn clause, and substitute all occurrences
of U in the normalized assumptions by its template to obtain a set of normalized constraints.
– Apply Farkas’ lemma to eliminate universal quantification to obtain new constraints with only
existential quantification over the unknown coefficients c i j , di j and the factors λ j .
– Use an off-the-shelf prover, such as Z3, to find a model of the unknown coefficients from their
constraints, and replace them back in the template to discover the actual definition of U .
5.7

Soundness of the lemma synthesis framework

We claim that our lemma synthesis framework is sound, that is, all lemmas synthesized by the
framework are semantically valid. We formally state the soundness in the following Theorem 5.3.
Theorem 5.3 (Soundness of the lemma synthesis). Given a normal goal entailment E which does
not contain any unknown relation and a set of valid input lemma L, if the lemma synthesis procedure
SynthesizeLemma returns a set of lemmas Lsyn , then all lemmas in Lsyn are semantically valid.
Proof. Figure 11 shows that all lemmas returned by SynthesizeLemma are directly discovered
by RefineAnte and RefineConseq. In addition, all lemmas returned by RefineConseq are realized by FineTuneConseq (Figure 14, line 38). Moreover, all lemmas discovered by RefineAnte and
FineTuneConseq are verified by Prove in a setting that disables the lemma synthesis (NoSyn) and
utilizes the valid lemma set L (Figure 12, line 31 and Figure 17, line 55). It follows from Proposition
4.2 that if Prove returns Valid⟨_⟩ when verifying a lemma, then the lemma is semantically valid.
Consequently, all lemmas returned by SynthesizeLemma are semantically valid.
□
6

EXPERIMENTS

We have implemented the lemma synthesis framework into a prototype prover, named SLS3 and
have conducted two experiments to evaluate its ability in proving entailments. Both the prover and
the experiment details are available online at https://songbird-prover.github.io/lemma-synthesis.
3 SLS

is built on top of an existing prover Songbird [Ta et al. 2016]; its name stands for “Songbird + Lemma Synthesis”

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:24

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

Table 1. Evaluation on the existing entailment benchmarks, where participants are Slide (Sld), Sleek (Slk),
Spen (Spn), Cyclist (Ccl), Songbird (Sbd) and our prototype prover SLS

slrd_indt

slrd_entl

sll_entl

Benchmark
Proved Entailments
Total Proving Time (s)
Average Time (s)
Lemma Syn
Lemma App
Category
#En Sld Slk Spn Ccl Sbd Sls Sld Slk Spn Ccl Sbd Sls Sld Slk Spn Ccl Sbd Sls #Lm T (s) A (s) O (%) #Cv #Sp #Cb
bolognesa 57 0 0 57 0 57 57 0.0 0.0 23.6 0.0 140.3 18.5 – – 0.41 – 2.46 0.32 0 0.0 – 0.0
0
0 0
clones
60 0 60 60 60 60 60 0.0 3.7 3.5 0.5 3.9 0.7 – 0.06 0.06 0.01 0.07 0.01 0 0.0 – 0.0
0
0 0
smallfoot 54 0 54 54 54 54 54 0.0 2.7 2.5 11.8 3.5 4.2 – 0.05 0.05 0.22 0.06 0.08 0 0.0 – 0.0
0
0 0
singly-ll
64 12 48 3 63 64 64 1.0 6.3 0.1 2.1 8.3 1.7 0.08 0.13 0.04 0.03 0.13 0.03 0 0.0 – 0.0
0
0 0
doubly-ll 37 14 17 9 29 25 35 38.3 3.1 0.4 112.5 11.3 91.9 2.74 0.18 0.04 3.88 0.45 2.63 18[10] 51.2 2.8 55.7 8 (68) 0 2 (2)
nested-ll 11 0 5 11 7 11 11 0.0 2.2 0.5 16.7 2.3 0.4 – 0.44 0.04 2.38 0.21 0.04 0 0.0 – 0.0
0
0 0
skip-list
13 0 4 13 5 13 13 0.0 1.1 1.1 0.6 8.1 1.3 – 0.27 0.08 0.11 0.63 0.10 0 0.0 – 0.0
0
0 0
tree
26 12 14 0 23 23 24 110.0 2.9 0.0 58.8 11.5 2.2 9.16 0.21 – 2.55 0.50 0.09 0 0.0 – 0.0
0
0 0
ll/ll2
24 0 0 0 24 24 24 0.0 0.0 0.0 60.2 11.9 78.5 – – – 2.51 0.50 3.27 14[10] 12.6 0.9 16.1 4 (4) 0 6 (11)
ll-even/odd 20 0 0 0 20 20 20 0.0 0.0 0.0 34.6 50.3 1.3 – – – 1.73 2.52 0.07 0 0.0 – 0.0
0
0 0
ll-left/right 20 0 0 0 20 20 20 0.0 0.0 0.0 19.5 10.6 1.3 – – – 0.97 0.53 0.06 0 0.0 – 0.0
0
0 0
misc.
32 0 0 0 31 32 32 0.0 0.0 0.0 254.2 55.0 19.5 – – – 8.20 1.72 0.61 2[2] 1.3 0.7 6.7 2 (3) 0 0
Total
418 38 202 207 336 403 414 149.2 21.9 31.6 571.5 317.2 221.6 3.93 0.11 0.15 1.70 0.79 0.54 34[22] 65.2 1.9 29.4 14 (75) 0 8 (13)

The first experiment was done on literature benchmarks, which include sll_entl, slrd_entl from
the separation logic competition SL-COMP 2014 [Sighireanu and Cok 2016], and slrd_indt by Ta
et al. [2016]. These benchmarks focus on representing the data structures’ shapes, hence, their
pure formulas solely contain equality constraints among spatial variables. Therefore, we decided to
compose a richer entailment benchmark slrd_lm, which captures also arithmetic constraints of the
data structures’ size and content, and then performed the second experiment. Moreover, we only
considered entailments that are marked as valid. Our experiments were conducted on a Ubuntu
14.04 LTS machine with CPU Intel® CoreTM i7-6700 (3.4GHz) and RAM 16GB. We compared SLS
against state-of-the-art separation logic provers, including Slide [Iosif et al. 2013], Sleek [Chin
et al. 2012], Spen [Enea et al. 2014], Cyclist [Brotherston et al. 2011] and Songbird [Ta et al. 2016].
These provers were configured to run with a timeout of 180 seconds for each entailment.
We present the first experiment in Table 1. The benchmark sll_entl relates to only singly linked list
and is categorized by its original sub-benchmarks. The two benchmarks slrd_entl and slrd_indt
are classified based on the related data structures, which are variants of linked lists and trees. We
report in each category the number of entailments successfully proved by each prover, where the
best results are in bold (the total number of entailments is shown in the column #En). We also
report the total and the average time in seconds of each prover for all proved entailments. To be fair,
time spent on unproved entailments are not considered since a prover might spend up to the timeout
of 180(s) for each such entailment. We also provide the statistics of how lemmas are synthesized and
applied by SLS. The numbers of lemmas synthesized and used are presented in the column #Lm,
where x[y] means that there are totally x lemmas synthesized, and only y of them are successfully
used. The total and the average time spent on synthesizing all lemmas are displayed in the columns
T and A. The synthesis overhead is shown in the column O, which is the percentage (%) of the total
synthesizing time over the total proving time. We also classify the synthesized lemmas into three
groups of conversion, split, and combination lemmas (#Cv, #Sp, and #Cb), in a spirit similar to the
motivating lemmas L 1 , L 2 and L 3 (Section 2). The number x(y) in each group indicates that there
are x lemmas applied, and they are repeatedly applied y times.
Table 1 shows that SLS can prove most of the entailments in existing benchmarks (414/418 ≈ 99%)
on an average of 0.54 seconds per entailment, which is 1.46 times faster than the second best
prover Songbird. Moreover, SLS outperforms the third best prover Cyclist in both the number of
proved entailments (more than 78 entailments) and the average proving time (3.15 times faster).
Other provers like Sleek, Spen and Slide can prove no more than 50% of the entailments that
SLS can prove. In addition, SLS achieves the best results in all categories, which demonstrates
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:25

Table 2. Evaluation on the benchmark slrd_lm, where • marks categories with arithmetic constraints
Benchmark slrd_lm
Category
#En
ll/rev
20
ll-even/odd
17
ll/rev+arith•
72
ll-sorted•
25
dll/rev/null
22
dll/rev/null+arith• 94
ll/dll-mixed
5
ll/dll-mixed+arith• 15
tree/tseg
18
tree/tseg+arith•
12
Total
300

Proved Entails
Ccl Sbd Sls
17 18
20
17 17 17
0 10
72
0 3
19
22 22 22
0 17
94
5 5
5
0 5
15
7 7
18
0 3
12
68 107 294

Proving Time (s)
Ccl Sbd Sls
446.5 87.1 205.0
3.5 0.6
0.4
0.0 0.4 203.2
0.0 0.1
8.7
8.4 17.6 149.8
0.0 27.6 2480.6
0.4 0.1
0.2
0.0 0.4 328.3
1.3 0.3 135.0
0.0 3.5 513.7
460.0 137.7 4024.8

Average Time (s)
Ccl Sbd Sls
26.27 4.84 10.25
0.21 0.03 0.02
– 0.04 2.82
– 0.03 0.46
0.38 0.80 6.81
– 1.63 26.39
0.07 0.03 0.03
– 0.08 21.89
0.18 0.04 7.50
– 1.15 42.81
6.76 1.29 13.69

Lemma Synthesis
#Lm
T (s) A (s) O (%)
28 [20] 8.1 0.3 3.9
0
0.0
– 0.0
81 [81] 50.9 0.6 25.1
14 [14] 4.9 0.3 55.8
12 [7] 59.1 4.9 39.5
236 [158] 1902.7 8.1 76.7
0
0.0
– 0.0
12 [10] 227.2 18.9 69.2
18 [12] 3.8 0.2 2.8
20 [16] 211.2 10.6 41.1
421 [318] 2467.7 5.9 61.3

Lemma Application
#Cv
#Sp
#Cb
18 (25)
0
2 (2)
0
0
0
0
81 (143)
0
0
0
14 (30)
7 (8)
0
0
74 (74) 69 (103) 15 (15)
0
0
0
8 (8)
2 (2)
0
8 (11)
0
4 (5)
8 (8)
4 (5)
4 (4)
123 (134) 156 (253) 39 (56)

the effectiveness of our lemma synthesis technique. Regarding the 4 entailments that SLS cannot
prove, they are related to the doubly linked list or the tree data structures (doubly-ll/tree), where
the needed lemmas are too complicated to be synthesized within a timeout of 180 seconds.
In the first experiment, the lemma synthesis is only triggered in some categories with an overhead
of 29.4%. Although this overhead is considerable, it does not overwhelm the overall proving process
since much of the proving time is saved via the lemma application. The lemma synthesis’s efficacy,
determined by the ratio of the number of lemmas applied to the number of lemmas synthesized, is
about 65% (22 lemmas used in the total of 34 lemmas synthesized). More interestingly, these 22
lemmas were applied totally 88 times. This fact implies that a lemma can be (re)used multiple times.
In this experiment, the conversion lemmas is applied more often than other lemmas (75/88 times).
In the second experiment, we apply the best three provers in the first experiment, i.e., Cyclist,
Songbird, and SLS, on the more challenging benchmark slrd_lm. This benchmark was constructed
by enhancing the existing inductive heap predicates with richer numeric properties of the data
structures’ size and content. These new predicates enable more challenging entailments to be
designed, such as the motivating entailment E 1 from Section 2.
E 1 ≜ dllrev(x, y, u, v, n) ∗ dll(v, u, z, t, 200) ∧ n≥100 |− ∃r .(dll(x, y, r , z, n+199) ∗ z7→r , t)

Details of the second experiment is presented in Table 2. Entailments in the benchmark slrd_lm are
categorized based on the participating heap predicates and their numeric properties. To minimize
the table’s size, we group various heap predicates related to the same data structure in one category.
For example, the category dll/rev/null contains entailments about doubly linked lists, including
normal lists (dll), reversed lists (dllrev), or null-terminated lists (dllnull). Entailments in the category
ll/dll-mixed involve both the singly and the doubly linked lists.
Table 2 shows that SLS outperforms other provers at all categories. In total, SLS can prove 98% of
the benchmark problems (294/300 entailments), which is 2.7 times better than the second best prover
Songbird (107/300 entailments). More impressively, in the 5 categories with arithmetic constraints,
marked by •, SLS can prove more than 5.5 times the number of entailments that Songbird can
(212 vs. 38 entailments). On the other hand, Cyclist performs poorly in this experiment because it
does not support numeric properties yet. However, among 82 non-arithmetic entailments, Cyclist
can prove 68 entailments (about 80%), whereas SLS can prove all of them.
In the second experiment, the lemma synthesis overhead is higher (61.3%) since there are many
lemmas synthesized (421). However, the overall efficacy is also improved (75.5%) when 318 synthesized lemmas are actually used to prove goal entailments. It is worth noticing that 100% lemmas
synthesized in the two arithmetic categories ll/rev+arith and ll-sorted are utilized; this shows the
usefulness of our proposed framework in proving sophisticated entailments. In this experiment, the
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:26

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

split lemmas are synthesized (49.1% of the total synthesized lemmas) and prominently used (57% of
the total number of lemma application). This interesting fact shows that the slrd_lm benchmark,
though handcrafted, was well designed to complement the existing benchmarks.
7

RELATED WORK

There have been various approaches proposed to prove separation logic entailments. A popular
direction is to restrict the inductive heap predicates to certain classes such as: predicates whose
syntax and semantics are defined beforehand [Berdine et al. 2004, 2005b; Bozga et al. 2010; Pérez and
Rybalchenko 2011, 2013; Piskac et al. 2013, 2014], predicates describing variants of linked lists [Enea
et al. 2014], or predicates satisfying a particular bounded tree width property [Iosif et al. 2013, 2014].
These restrictions enable the invention of practical and effective entailment proving techniques.
However, these predicate classes cannot model sophisticated constraints of data structures, which
involve not only the shape but also the size or the content, like the predicates dll and dllrev in
Section 2. In addition, the existing techniques are tied to fixed sets of inductive heap predicates and
could not be automatically extended to handle new predicates. This extension requires extra efforts.
Another research direction is to focus on a broader class of user-defined inductive heap predicates.
In particular, Chin et al. [2012] proposed a proof system based on the unfold-and-match technique:
heap predicates in a goal entailment can be unfolded by their definitions to produce possibly
identical predicates in the antecedent and consequent, which can be matched and removed to derive
simpler sub-goal entailments. However, an inductive heap predicate can be unfolded infinitely
often, which leads to the infinite derivation of an entailment proof. To deal with such situation,
Brotherston et al. [2011] and Chu et al. [2015] proposed inspiring techniques respectively based
on cyclic and induction proofs where the infinite unfolding sequences can be avoided by induction
hypothesis applications. In their works, the induction hypotheses are discovered directly from the
candidate entailments; they might not be sufficiently general to prove sophisticated entailments.
Therefore, these entailments’ proofs often require the supporting lemmas, such as L 1 , L 2 , L 3 (Section
2). These lemmas are also needed by other non-induction based verification systems, such as [Chin
et al. 2012; Qiu et al. 2013]. At present, these systems require users to manually provide the lemmas.
To the best of our knowledge, there have been two approaches aiming to automatically discover
the supporting lemmas. The first approach is the mutual induction proof presented in [Ta et al.
2016]. This work speculates lemmas from all entailments which are already derived in an ongoing induction proof to assist in proving future entailments introduced within the same proof.
This speculation provides more lemma/induction hypothesis candidates than the cyclic-based
[Brotherston et al. 2011] and induction-based [Chu et al. 2015] techniques. Consequently, it can
increase the chance of successfully proving the entailments. However, the mutual induction proof
cannot handle sophisticated entailments, such as E 1 in Section 2. All entailments derived from E 1
may contain specific constraints and cannot be applied to prove other derived entailments.
The second approach is the lemma generation presented in [Enea et al. 2015]. This work considers
an interesting class of inductive heap predicates satisfying the notions of compositionality and completion. Under these properties, a class of lemmas can be enumerated beforehand, either to convert
inductive predicates of the same arity, or to combine two inductive predicates. However, this technique cannot generate lemmas which convert predicates of different arities, or combine a singleton
heap predicate with an inductive heap predicate, or split an inductive heap predicate into other predicates. In addition, an inductive heap predicate satisfying the compositionality property has exactly
one base-case definition, whose heap part is also empty. Moreover, each inductive-case definition
must contain a singleton heap predicate whose root address is one of the inductive heap predicate’s
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:27

arguments, like the compositional predicate ls(x, y) = (x=y) ∨ ∃u.(x7→u ∗ ls(u, y)). This technique,
therefore, cannot generate lemmas for predicates with non-empty base cases, e.g., dll and dllrev in
Section 2, or lemmas for the predicates defined in a reverse-fashion, like the non-compositional preddef
icate lsrev(x, y) = (x=y) ∨ ∃u.(lsrev(x, u) ∗ u7→y). These reverse-fashion predicates are prevalent in
SL-COMP 2014’s benchmarks, such as RList, ListO, DLL_plus, DLL_plus_rev, DLL_plus_mid.
def

In the synthesis context, there is an appealing approach called SyGuS, a.k.a., Syntax-Guided Synthesis [Alur et al. 2015]. This approach aims to infer computer programs satisfying certain restrictions
on its syntax and semantics (respectively constrained by a context free grammar and a SMT formula). Techniques following SyGuS often operate on a learning phase which proposes a candidate
program, and a verification phase which checks the proposal against the semantic restriction. To
some extent, our lemma synthesis approach is similar to SyGuS since we also discover potential
lemmas and verify their validity. However, we focus on synthesizing separation logic lemmas but
not the computer programs. Our syntactic restriction is more goal-directed since the lemmas is
controlled by specific templates, unlike the context-free-grammar restriction of SyGuS. Moreover,
our semantic restriction cannot be represented by a SMT formula since we require that if a lemma
can be proved valid, its proof must contain an induction hypothesis application. Therefore, we
believe that the induction proof is necessary in both the lemma discovery and verification phases.
This proof technique is currently not supported by any SyGuS-based approaches.
8

CONCLUSION

We have proposed a novel framework for synthesizing lemmas to assist in proving separation logic
entailments in the fragment of symbolic-heap separation logic with inductive heap predicates and
linear arithmetic. Our framework is able to synthesize various kinds of inductive lemmas, which
help to modularize the proofs of sophisticated entailments. The synthesis of inductive lemmas is
non-trivial since induction proof is required by both the lemma discovery and validation phases. In
exchange, these lemmas can significantly improve the completeness of induction proof in separation
logic. We have shown by experiment that our lemma-synthesis-assisted prover SLS is able to prove
many entailments that could not be proved by the state-of-the-art separation logic provers.
We shall now discuss two limitations of our approach. Firstly, our current implementation cannot
simultaneously derive new constraints from both the antecedent and the consequent of a lemma
template. Theoretically, our framework can handle a lemma template with different unknown
relations on both these two sides. However, the set of unknown assumptions which is introduced
corresponding to these relations is far too complicated to be discharged by the current underlying
prover. Secondly, we only support to infer linear arithmetic constraints with Farkas’ lemma. In
future, we would like to extend the lemma synthesis framework with suitable constraint solving
techniques to support more kinds of pure constraints, such as sets or multisets of values.
ACKNOWLEDGMENTS
We would like to thank the reviewers of POPL’18 PC and AEC for the constructive comments on the
paper and the artifact. We wish to thank Dr. Aleksandar Nanevski for his valuable suggestions on
preparing the final version of this paper, and Dr. Andrew C. Myers for his dedication as the program
chair of POPL’18. We are grateful for the encouraging feedback from the reviewers of OOPSLA’17 on
our previous submission. The first author wish to thank Ms. Mirela Andreea Costea and Dr. Makoto
Tatsuta for the inspiring discussions about the entailment proof. This research is partially supported
by an NUS research grant R-252-000-553-112 and an MoE Tier-2 grant MOE2013-T2-2-146.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:28

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

REFERENCES
Aws Albarghouthi, Josh Berdine, Byron Cook, and Zachary Kincaid. 2015. Spatial Interpolants. In European Symposium on
Programming (ESOP). 634–660.
Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan,
Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama,
Emina Torlak, and Abhishek Udupa. 2015. Syntax-Guided Synthesis. In Dependable Software Systems Engineering. 1–25.
Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2004. A Decidable Fragment of Separation Logic. In International
Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 97–109.
Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005a. Smallfoot: Modular Automatic Assertion Checking with
Separation Logic. In International Symposium on Formal Methods for Components and Objects. 115–137.
Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005b. Symbolic Execution with Separation Logic. In Asian
Symposium on Programming Languages and Systems (APLAS). 52–68.
Josh Berdine, Byron Cook, and Samin Ishtiaq. 2011. SLAyer: Memory Safety for Systems-Level Code. In International
Conference on Computer Aided Verification (CAV). 178–183.
Marius Bozga, Radu Iosif, and Swann Perarnau. 2010. Quantitative Separation Logic and Programs with Lists. J. Autom.
Reasoning 45, 2 (2010), 131–156.
James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. 2011. Automated Cyclic Entailment Proofs in
Separation Logic. In International Conference on Automated Deduction (CADE). 131–146.
James Brotherston, Carsten Fuhs, Juan A. Navarro Pérez, and Nikos Gorogiannis. 2014. A decision procedure for satisfiability
in Separation Logic with inductive predicates. In Joint Meeting of International Conference on Computer Science Logic and
Symposium on Logic in Computer Science, CSL-LICS. 25:1–25:10.
James Brotherston, Nikos Gorogiannis, Max I. Kanovich, and Reuben Rowe. 2016. Model checking for Symbolic-Heap
Separation Logic with inductive predicates. In Symposium on Principles of Programming Languages (POPL). 84–96.
James Brotherston and Alex Simpson. 2011. Sequent calculi for induction and infinite descent. J. Log. Comput. 21, 6 (2011),
1177–1216.
Alan Bundy. 2001. The Automation of Proof by Mathematical Induction. In Handbook of Automated Reasoning (in 2 volumes).
845–911.
Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O’Hearn,
Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. 2015. Moving Fast with Software Verification. In NASA
International Symposium on Formal Methods (NFM). 3–11.
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. 2012. Automated verification of shape, size and
bag properties via user-defined predicates in Separation Logic. Science of Computer Programming (SCP) 77, 9 (2012),
1006–1036.
Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh. 2015. Automatic induction proofs of data-structures in imperative
programs. In Conference on Programming Language Design and Implementation (PLDI). 457–466.
Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint
Solving. In International Conference on Computer Aided Verification (CAV). 420–432.
Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, and James Worrell. 2011. Tractable Reasoning in a
Fragment of Separation Logic. In International Conference on Concurrency Theory (CONCUR). 235–249.
Dino Distefano and Matthew J. Parkinson. 2008. jStar: towards practical verification for java. 213–226.
Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. 2014. Compositional Entailment Checking for a
Fragment of Separation Logic. In Asian Symposium on Programming Languages and Systems (APLAS). 314–333.
Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. 2015. On Automated Lemma Generation for Separation Logic with
Inductive Definitions. In International Symposium on Automated Technology for Verification and Analysis (ATVA). 80–96.
Radu Iosif, Adam Rogalewicz, and Jiri Simácek. 2013. The Tree Width of Separation Logic with Recursive Definitions. In
International Conference on Automated Deduction (CADE). 21–38.
Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. 2014. Deciding Entailments in Inductive Separation Logic with Tree
Automata. In International Symposium on Automated Technology for Verification and Analysis (ATVA). 201–218.
Quang Loc Le, Jun Sun, and Wei-Ngan Chin. 2016. Satisfiability Modulo Heap-Based Programs. In International Conference
on Computer Aided Verification (CAV). 382–404.
Leonardo Mendonça De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In International Conference on Tools
and Algorithms for Construction and Analysis of Systems (TACAS). 337–340.
Huu Hai Nguyen and Wei-Ngan Chin. 2008. Enhancing Program Verification with Lemmas. In International Conference on
Computer Aided Verification (CAV). 355–369.
Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures.
In International Conference on Computer Science Logic (CSL). 1–19.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:29

Juan Antonio Navarro Pérez and Andrey Rybalchenko. 2011. Separation Logic + Superposition Calculus = Heap Theorem
Prover. In Conference on Programming Language Design and Implementation (PLDI). 556–566.
Juan Antonio Navarro Pérez and Andrey Rybalchenko. 2013. Separation Logic Modulo Theories. In Asian Symposium on
Programming Languages and Systems (APLAS). 90–106.
Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013. Automating Separation Logic Using SMT. In International
Conference on Computer Aided Verification (CAV). 773–789.
Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. Automating Separation Logic with Trees and Data. In International
Conference on Computer Aided Verification (CAV). 711–728.
William Pugh. 1991. The Omega Test: a fast and practical integer programming algorithm for dependence analysis. In
Proceedings Supercomputing ’91, Albuquerque, NM, USA, November 18-22, 1991. 4–13.
Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy Madhusudan. 2013. Natural proofs for structure, data,
and separation. In Conference on Programming Language Design and Implementation (PLDI). 231–242.
John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Symposium on Logic in Computer
Science (LICS). 55–74.
John C. Reynolds. 2008. An Introduction to Separation Logic. Lecture Notes for the PhD Fall School on Logics and Semantics
of State, Copenhagen 2008. Retrieved on 2017, March 16th. http://www.cs.cmu.edu/~jcr/copenhagen08.pdf
Alexander Schrijver. 1986. Theory of Linear and Integer Programming. John Wiley & Sons, Inc., New York, NY, USA.
Mihaela Sighireanu and David R. Cok. 2016. Report on SL-COMP 2014. Journal on Satisfiability, Boolean Modeling and
Computation 9 (2016), 173–186.
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2016. Automated Mutual Explicit Induction Proof
in Separation Logic. In International Symposium on Formal Methods (FM). 659–676.
Alfred North Whitehead and Bertrand Russell. 1912. Principia Mathematica. University Press.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:30
A

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
SOUNDNESS PROOF

A.1

Soundness of inference rules

We prove soundness of inference rules in Section 4 by showing that if entailments in their premises
are valid, and their side conditions, if any, are satisfied, then goal entailments in their conclusions
are also valid.
1. Axiom rules |−Π , ⊥1L , ⊥2L
|−Π

H, L, Π 1 |− Π 2

Π 1 →Π2

⊥1L

ι1

ι2

H, L, F 1 ∗ u 7→v® ∗ u 7→t® |− F 2

⊥2L

H, L, F 1 ∧ Π 1 |− F 2

Π1 →false

– When the rule |−Π is applied, SMT solvers or theorem provers, such as Z3 [Moura and Bjørner
2008] or Omega Calculator [Pugh 1991], can be invoked to check the side condition: Π 1 → Π 2 .
If this side condition holds, then clearly the entailment Π 1 |− Π 2 is valid.
– For the two rules ⊥1L , ⊥2L , it is easy to verify their goal entailments’ antecedents are unsatisfiable
ι1
ι2
since they either contain an overlapped singleton heap (u 7→v® ∗ u 7→t® in the rule ⊥1L ), or a
contradiction (Π 1 → false in the rule ⊥1L ). Therefore, these entailments are evidently valid.
2. Rule =L , ∃L , ∃R
=L

H, L, F 1 [u/v] |− F 2 [u/v]
H, L, F 1 ∧ u=v |− F 2

∃L

H, L, F 1 [u/x] |− F 2
H, L, ∃x .F 1 |− F 2

u < FV(F 2 )

∃R

x .F 2 [u/v]
H, L, F 1 |− ∃®
H, L, F 1 |− ∃®
x, v.(F 2 ∧ u=v)

– For the rule =L , consider an arbitrary model s, h of the goal entailment’s antecedent. Then
s, h |= F 1 ∧ u=v. It follows that s(u) = s(v), therefore s, h |= F 1 [u/v]. Since the entailment
F 1 [u/v] |− F 2 [u/v] in the rule’s premise is valid, it implies s, h |= F 2 [u/v]. This means s, h |= F 2 ,
due to s(u) = s(v). Therefore, F 1 ∧ u=v |− F 2 is valid.
– To prove correctness of the rule ∃L , we consider an arbitrary model s, h such that s, h |= ∃x .F 1 .
By semantics of the ∃ quantification, there is an integer value v ∈ Int such that s ′, h |= F 1 , with
s ′ = [s |x:v]. Then s ′′, h |= F 1 [u/x] with s ′′ is extended from s ′ such that s ′′(u) = s ′(x). Since
s ′ = [s |x:v], it follows that s ′′ = [s |u:v]. On the other hand, given that entailment in the rule’s
premise is valid, then s ′′, h |= F 2 . It implies that [s |u:v] |= F 2 . In addition u < FV(F 2 ). Therefore
s, h |= F 2 . Since s, h is chosen arbitrarily, it follows that the rule ∃L is correct.
– Correctness of ∃R is straight forward. Suppose that s, h is an arbitrary model such that s, h |= F 1 .
Since entailment in the rule’s premise is valid, then s, h |= F 2 [e/x]. It follows that s, h also satisfies
∃x .F 2 , by simply choosing value v of x such that v = ⟦e⟧s . Since s, h is chosen arbitrarily, it
follows that the entailment in the rule’s conclusion is valid. Therefore ∃R is valid.
3. Rule EL and ER
EL

H, L, F 1 |− F 2
H, L, F 1 ∗ emp |− F 2

ER

H, L, F 1 |− ∃®
x .F 2
H, L, F 1 |− ∃®
x .(F 2 ∗ emp)

– It is evident that two formulas F 1 ∗ emp and F 1 in the rule EL are semantically equivalent. In
addition, F 2 ∗ emp and F 2 in the rule ER are also semantically equivalent. It follows that both the
two rules EL and ER are correct.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:31

4. Rule CA
CA

H, L, F 1 ∧ Π |− F 2
H, L, F 1 ∧ ¬Π |− F 2
H, L, F 1 |− F 2

– The rule’s premises provide that both the two entailments F 1 ∧ Π |− F 2 and F 1 ∧ ¬Π |− F 2 are
valid. For an arbitrary model s, h such that s, h |= F 1 , we consider two cases as follows.
(1) s, h |= F 1 ∧ Π. Since F 1 ∧ Π |− F 2 is valid, it follows that s, h |= F 2 .
(2) s, h ̸ |= F 1 ∧ Π. Since s, h |= F 1 , it follows that s, h ̸ |= Π. Consequently, s, h |= ¬Π, by the
semantics of separation logic formulas. We have shown that s, h |= F 1 and s, h |= ¬Π, it
implies that s, h |= F 1 ∧ ¬Π. Since F 1 ∧ ¬Π |− F 2 is valid, it follows that s, h |= F 2 .
In both the above cases, we show that for an arbitrary model s, h, if s, h |= F 1 , then s, h |= F 2 .
Therefore, the entailment F 1 |− F 2 in the conclusion of the rule CA is valid.
5. Rule ∗7→ and ∗P
∗7→

H, L, F 1 |− ∃®
x .(F 2 ∧ u=t ∧ v=
® w)
®
ι

ι

H, L, F 1 ∗ u 7→v® |− ∃®
x .(F 2 ∗ t 7→w)
®

u < x,
® v® # x®

∗P

x .(F 2 ∧ u=
® v)
®
H, L, F 1 |− ∃®
u® # x®
H, L, F 1 ∗ P(®
u) |− ∃®
x .(F 2 ∗ P(v))
®
ι

– To prove the rule ∗7→, we consider an arbitrary model s, h such that s, h |= F 1 ∗u 7→v.
® Then, there
ι
|
|
exists h 1 # h 2 such that h = h 1 ◦ h 2 , and s, h 1 = F 1 , and s, h 2 = u 7→v.
® On one hand, entailment
in the rule’s premise is valid, it follows that s, h 1 |= ∃®
x .(F 2 ∧ u=t ∧ v=
® w).
® By semantics of ∃
quantification, s ′, h 1 |= F 2 ∧ u=t ∧ v=
® w,
® with s ′ is a model extended from s with integer values
of x.
® On the other hand, the rule’s side condition gives u < x,
® and v® # x,
® and s ′ is extend from s
ι
ι
′
with values of x,
® and s, h 2 |= u 7→v,
® it follows that s , h 2 |= u 7→v.
® Combining these two hands,
ι
′
with the fact that h 1 # h 2 and h = h 1 ◦ h 2 , the following holds: s , h |= F 2 ∗ u 7→v® ∧ u=t ∧ v=
® w.
® By
ι
semantics of equality (=), the following also holds: s ′, h |= F 2 ∗ t 7→w® ∧u=t ∧ v=
® w.
® By weakening
ι
this formula via dropping the condition u=t ∧ v=
® w,
® it is evident that s ′, h |= F 2 ∗ t 7→w.
® Since
ι
s ′ is extended from s with values of x,
® it is evident that s, h |= ∃®
x .(F 2 ∗ t 7→w).
® Recall that s, h is
chosen arbitrarily, this implies that the rule ∗7→ is sound.
– Soundness of ∗P can be proved in the similar way with the rule ∗7→ above.
6. Rule PR
PR

H, L, F 1 |− ∃®
x .(F 2 ∗ FiP (®
u))
x .(F 2 ∗ P(®
u))
H, L, F 1 |− ∃®

def

F iP (u)
® ⇒ P(u)
®

– Consider an arbitrary model s, h such that s, h |= F 1 . Since entailment in the rule’s premise is
u)). In addition, the rule’s side condition that FiP (®
valid, it follows that s, h |= ∃®
x .(F 2 ∗ FiP (®
u) is
one of the definition cases of P(®
u) clearly implies that s, h |= ∃®
x .(F 2 ∗ P(®
u)). Since s, h is chosen
arbitrarily, it follows that entailment in the rule’s conclusion is valid.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:32

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

7. Rule ID
H ′, L, Σ1 ∗ F 1P (®
u) ∧ Π 1 |− F 2
ID

...

P (®
H ′, L, Σ1 ∗ Fm
u) ∧ Π 1 |− F 2

H, L, Σ1 ∗ P(®
u) ∧ Π1 |− F 2

P (u);
P(u)
® = F 1P (u)
® ∨ ... ∨ Fm
® †
def

† : H ′ ≜ H ∪ {H }, where H is obtained by freshly renaming all variables of Σ1 ∗ P(®
u) ∧ Π1 |− F 2
P (®
– We show that if all of the entailments F 1 ∗ F 1P (®
u) |− F 2 , . . . , F 1 ∗ Fm
u) |− F 2 in the rule premise
are valid, then so is the entailment F 1 ∗ P(®
u) |− F 2 in the conclusion.

Indeed, consider an arbitrary model s, h such that s, h |= F 1 ∗ P(®
u). The side condition of the rule
P (®
P (®
gives that P(®
u) ≜ F 1P (®
u) ∨ . . . ∨ Fm
u), i.e., F 1P (®
u), . . . , Fm
u) are all definition cases of P(®
u). Since
s, h |= F 1 ∗ P(®
u), it follows that s, h |= F 1 ∗ FiP (®
u), for all i = 1 . . . m. On the other hand, F 1 ∗ F 1P (®
u),
P
. . . , F 1 ∗ Fm (®
u) are antecedents of all entailments in this rule’s premises, and these entailments
have the same consequent F 2 . Therefore, s, h |= F 2 . Since s, h is chosen arbitrarily, it follows that
entailment in the rule’s conclusion is valid. This confirms soundness of the rule ID.
8. Rule IH:
IH

H ∪ {Σ3 ∗ P(v)
® ∧ Π3 |− F 4 }, L, F 4θ ∗ Σ ∧ Π1 |− F 2 P(u)
® ≺ P(v);
®
∃θ,
Σ.(Σ
∗ P(u)
®  Σ3 θ ∗ P(v)θ
® ∗ Σ) ∧ (Π1 →Π3 θ )
1
u) ∧ Π 1 |− F 2
H ∪ {Σ3 ∗ P(v)
® ∧ Π3 |− F 4 }, L, Σ1 ∗ P(®

– The rule’s side conditions Σ1 ∗ P(®
u)  Σ3θ ∗ P′(v)θ
® ∗ Σ and Π 1 →Π 3θ imply that the entailment
Σ1 ∗ P(®
u) ∧ Π 1 |− Σ3θ ∗ P′(v)θ
® ∗ Σ ∧ Π 3θ ∧ Π 1 is valid.
By applying Theorem 3.8, the induction hypothesis Σ3 ∗ P′(v)
® ∧ Π 3 |− F 4 implies that Σ3θ ∗
′
|
P (v)θ
® ∧ Π 3θ − F 4θ is valid. It follows that the following entailment is also valid: Σ3θ ∗ P′(v)θ
® ∗
Σ ∧ Π 3θ ∧ Π 1 |− F 4θ ∗ Σ ∧ Π 1 .
We have shown that the two entailments Σ1 ∗ P(®
u) ∧ Π 1 |− Σ3θ ∗ P′(v)θ
® ∗ Σ ∧ Π 3θ ∧ Π 1 and
′
Σ3θ ∗ P (v)θ
® ∗ Σ ∧ Π 3θ ∧ Π 1 |− F 4θ ∗ Σ ∧ Π 1 are valid. In addition, the rule’s premise gives
that F 4θ ∗ Σ ∧ Π 1 |− F 2 is valid. It follows that the entailment Σ1 ∗ P(®
u) ∧ Π1 |− F 2 in the rule’s
conclusion is valid as well. Therefore, the rule IH is correct.
9. Rule LML , LMR :
H, L ∪ {Σ3 ∧ Π 3 |− F 4 }, F 4θ ∗ Σ ∧ Π1 |− F 2
LML

LMR

H, L ∪ {Σ3 ∧ Π 3 |− F 4 }, Σ1 ∧ Π 1 |− F 2

∃θ, Σ. (Σ1  Σ3θ ∗ Σ) ∧ (Π1 →Π 3θ )

H, L ∪ {F 3 |− ∃w.(Σ
® 4 ∧ Π 4 )}, F 1 |− ∃®
x .(F 3θ ∗ Σ ∧ Π 2 )
® 4 ∧ Π4 )}, F 1 |− ∃®
x .(Σ2 ∧ Π 2 )
H, L ∪ {F 3 |− ∃w.(Σ

∃θ, Σ. (Σ4θ ∗ Σ  Σ2 ) ∧ (wθ
® ⊆ x)
®

– Soundness of the lemma application rule LML can be proved similar to IH. Specifically, this rule’s
side conditions Σ1  Σ3θ ∗ Σ and Π 1 →Π 3θ imply that the entailment Σ1 ∧ Π 1 |− Σ3θ ∗ Σ ∧ Π 3θ ∧ Π 1
is valid. On the other hand, by applying Theorem 3.8, the lemma Σ3 ∧ Π 3 |− F 4 implies that
the entailment Σ3θ ∧ Π 3θ |− F 4θ is valid. It follows that the following entailment is also valid:
Σ3θ ∗ Σ ∧ Π 3θ ∧ Π 1 |− F 4θ ∗ Σ ∧ Π 1 . We have shown that both the two entailments Σ1 ∧ Π 1 |−
Σ3θ ∗ Σ ∧ Π 3θ ∧ Π 1 and Σ3θ ∗ Σ ∧ Π 3θ ∧ Π 1 |− F 4θ ∗ Σ ∧ Π 1 are valid. In addition, this rule’s
premise provides that the entailment F 4θ ∗ Σ ∧ Π 1 |− F 2 is also valid. Consequently, the goal
entailment Σ1 ∧ Π 1 |− F 2 is valid as well. Therefore, soundness of the rule LML is claimed.
® 4 is valid, therefore
® 4 ∧ Π 4 ) implies that F 3 |− ∃w.Σ
– For the rule LMR , the lemma F 3 |− ∃w.(Σ
F 3θ |− ∃wθ
® .Σ4θ is also valid by Theorem 3.8. It follows that F 3θ ∗ Σ ∧ Π 2 |− ∃wθ
® .(Σ4θ ∗ Σ ∧ Π 2 )
is also valid. In addition, this rule’s side condition provides that wθ
® ⊆ x,
® therefore F 3θ ∗ Σ ∧

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic

9:33

Π 2 |− ∃®
x .(Σ4θ ∗ Σ ∧ Π 2 ) is valid. Furthermore, the rule’s premise provides that the entailment
F 1 |− ∃®
x .(F 3θ ∗ Σ ∧ Π 2 ) is valid. Hence, by Theorem 3.6, the entailment F 1 |− ∃®
x .(Σ4θ ∗ Σ ∧ Π 2 )
is valid. On the other hand, the rule’s side condition Σ4θ ∗ Σ  Σ2 implies that the entailment
x .(Σ4θ ∗Σ∧Π 2 )
Σ4θ ∗Σ∧Π 2 |− Σ2 ∧Π 2 is valid. We have shown that both the two entailments F 1 |− ∃®
and Σ4θ ∗ Σ ∧ Π 2 |− Σ2 ∧ Π 2 are valid, it follows by Theorem 3.6 again that the goal entailment
x .(Σ2 ∧ Π2 ) is also valid. Correctness of the rule LMR , therefore, is claimed.
F 1 |− ∃®
A.2

Soundness of the synthesis rules

We now present soundness proof the synthesis rules, presented in Figure 9, by showing that if
all assumptions and entailments in their premises are valid, and their side conditions, if any, are
satisfied, then goal entailments in their conclusions are also valid.
1. Rule U1Π and U2Π
U1Π

A ≜ {Π 1 ∧ U (®
x) → Π 2 }

U2Π

H, L, Π 1 ∧ U (®
x) |− Π 2

A ≜ {Π1 → ∃w.(Π
® 2 ∧ U (®
x))}
H, L, Π1 |− ∃w.(Π
® 2 ∧ U (®
x))

– Consider an arbitrary model s, h such that s, h |= Π 1 ∧ U (®
x). Since the unknown assumption
Π 1 ∧ U (®
x) → Π 2 is assumed valid, then it follows from the semantics of → that s, h |= Π 2 . Since
s, h is chosen arbitrarily, it follows that the goal entailment Π 1 ∧ U (®
x) |− Π 2 is also valid.
– The proof of the rule U2Π is similar to the proof of U1Π .
2. Rule U1Σ and U2Σ
U1Σ

A ≜ {Π 1 ∧ U (®
x) → false}
H, L, Σ1 ∧ Π1 ∧ U (®
x) |− Π 2

Σ1 ,emp

U2Σ

A ≜ {Π1 ∧ U (®
x) → false}
H, L, Π 1 ∧ U (®
x) |− ∃w.(Σ
® 2 ∧ Π2 )

Σ2 ,emp

– If the unknown assumption Π 1 ∧ U (®
x) → false in the premise of the rule U1Σ is valid, then it is
evident that Π 1 ∧ U (®
x) ≡ false, since only false can prove false. It follows that Σ1 ∧ Π 1 ∧ U (®
x) ≡
false. Consequently, the goal entailment Σ1 ∧ Π 1 ∧ U (®
x) |− Π 2 is valid, since its antecedent is a
contradiction.
x) → false in the rule’s
– Soundness proof the rule U2Σ is similar where the assumption Π 1 ∧ U (®
premise also implies that the goal entailment’s antecedent is a contradiction (Π 1 ∧ U (®
x) ≡ false)
3. Rule UIH
H ∪ {Σ3 ∗ P(v)
® ∧ Π 3 ∧ U (®
y) |− F 4 }, L, F 4θ ∗ Σ ∧ Π 1 |− F 2
UIH

A ≜ {Π1 ∧ U (®
x) → (Π3 ∧ U (®
y))θ }

u) ∧ Π 1 ∧ U (®
x) |− F 2
H ∪ {Σ3 ∗ P(v)
® ∧ Π3 ∧ U (®
y) |− F 4 }, L, Σ1 ∗ P(®
with † : P(®
u) ≺ P(v);
® ∃θ, Σ. (Σ1 ∗ P(®
u)  Σ3θ ∗ P(v)θ
® ∗ Σ)

†

– Since the rule UIH applies an induction hypothesis, which contains an unknown relation, to prove
another unknown entailment, the soundness of this rule can be proved in a similar manner to
the normal induction hypothesis application rule IH. Note that in the proof of UIH , although the
side condition Π 1 ∧ U (®
x) → Π 3θ ∧ U (®
y)θ contains unknown relations U (®
x) and U (®
y)θ , validity
of this side condition is clearly implied by the assumption A≜{Π 1 ∧ U (®
x) → Π 3θ ∧ U (®
y)θ } in
the rule’s premises.

A.3

Soundness proofs of Propositions 4.1, 4.2, 4.3

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:34

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

Proposition 4.1 (Proof of an unknown entailment). Given an unknown entailment E. If the
procedure Prove returns Valid⟨_⟩ and generates an assumption set A when proving E in the lemmasynthesis-disabled mode (NoSyn), using an empty induction hypothesis set (H =∅) and a valid lemma
set L as its inputs, then E is semantically valid, given that all assumptions in A are valid.
Proposition 4.2 (Proof of a normal entailment when the lemma synthesis is disabled).
Given a normal entailment E which does not contain any unknown relation. If the procedure Prove
returns Valid⟨_⟩ when proving E in the lemma-synthesis-disabled mode (NoSyn), using an empty
induction hypothesis set (H =∅) and a valid lemma set L as its inputs, then E is semantically valid.
Proposition 4.3 (Proof of a normal entailment when the lemma synthesis is enabled).
Given a normal entailment E which does not contain any unknown relation. If the procedure Prove returns Valid⟨_⟩ and synthesizes a set of lemmas Lsyn when proving E in the lemma-synthesis-enabled
mode (SynLM), using an empty induction hypothesis set (H =∅) and a valid lemma set L as its inputs,
then the entailment E and all lemmas in Lsyn are semantically valid.
Proof of Propositions 4.1, 4.2, 4.3. We have argued in Sections A.1 and A.2 that all of our inference
rules and synthesis rules are sound. In addition, our proof system, without the lemma synthesis
component, is clearly an instance of Noetherian induction where the sub-structural relation is
proved to be well-founded (Theorem 3.13) and is utilized by the induction hypothesis application
rule IH. Therefore, soundness of the proof system, when the lemma synthesis is disabled (Prove
is invoked with mode = NoSyn), is guaranteed by the Noetherian induction principle and the
soundness of all inference and synthesis rules. Now, we consider each proposition as follows.
– In Proposition 4.1, the proof system is invoked in the lemma-synthesis-disabled mode (NoSyn).
Based on our argument above about the proof system’s soundness in this mode, it is clear that
if Prove returns Valid⟨_⟩ and generates a set of assumptions A when proving the unknown
entailment E, then E is semantically valid given that all unknown assumptions in A are valid.
– In Proposition 4.2, the proof system is also invoked in the lemma-synthesis-disabled mode
(NoSyn). Since the goal entailment does not contain any unknown relation, there is no unknown
assumption introduced while proving E. Hence, if Prove returns Valid⟨_⟩, then E is semantically
valid.
– In Proposition 4.3, the proof system can synthesize a set of new lemma Lsyn when proving E.
Hence, we rely on the soundness of the lemma synthesis framework (Section 5) to argue about
the soundness of the proof system. Details about the lemma synthesis’s soundness are presented
in Theorem 5.3. Now, suppose that the lemma synthesis is already proved sound, then all lemmas
synthesized in Lsyn are semantically valid. Following that, we can separate the proof derivation
of E into multiple phases, in which the auxiliary phases are used to synthesize all lemmas in
Lsyn , and the main phase is to prove E, using both the input lemmas in L or the new synthesized
lemmas in Lsyn . Certainly, this main phase reflects the structural induction aspect of our proof
system, without the lemma synthesis component. In addition, all lemmas given in L and Lsyn
are valid. Therefore, if Prove returns Valid⟨_⟩ when proving E, then E is semantically valid. □

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic
B

9:35

FORMAL VERIFICATION OF THE PROOF SYSTEM
H1 , L1 , F 11 |− F 21

...

R

Hn , Ln , F 1n |− F 2n

A ≜ {Π 1 → Π 2 }

H, L, F 1 |− F 2

†

Fig. 19. General form of inference or synthesis rules

In Figure 19, we present a general form of an inference rule or a synthesis rule R where H, L, F 1 |−
F 2 is the rule’s conclusion; (H1 , L1 , F 11 |− F 21 ) , . . . , (Hn , Ln , F 1n |− F 2n ) and A are premises
corresponding to the derived sub-goal entailments and the unknown assumption set; and † is the
rule’s side condition. We define the retrieval functions Asms(R), Prems(R), and Concl(R) to extract
these components of the rule R, as follows:
Asms(R)

≜

{Π 1 → Π 2 }

Prems(R) ≜

n
{Hi , Li , F 1i |−F 2i }i=1

Concl(R) ≜

(H, L, F 1 |−F 2 )

Note that the first two functions Asms(R) and Prems(R) may return an empty set. Moreover, with
respect to the set R of all inference and synthesis rules given in Figures 6, 7, 8, and 9, we always
have L = Li .
Due to the soundness of these rules, we have:
Ó
valid(A) ∧ ni=1 valid ID (Hi , Li , F 1i |−F 2i ) → valid ID (H, L, F 1 |−F 2 ).
From this, we define the predicate sound(R) to denote the soundness of a rule R ∈ R as follows:
sound(R) ≜ valid(Asms(R)) ∧ valid ID (Prems(R)) → valid ID (Concl(R)).
The soundness of each inference or synthesis rule R, which is proved in Appendix A.1 or A.2, is
always assured at the beginning of the formal verification for each procedure in our framework.
Therefore, this assurance clearly connects the soundness of our procedures to the soundness of
these rules. Such guarantee can be considered as an invariant of the set of all rules R exploited in
these procedures. We denote the invariant as sound(R) ≜ ∀R ∈ R. sound(R), which specifies that
every rule R ∈ R is sound.
Below are the specifications of two retrieval procedures Assumptions(R) and Premises(R) to get
the set of assumptions and the set of premises from R.
Procedure Assumptions(R) // Retrieve assumptions on unknown relations in R
Requires: true
Ensures: res = Asms(R)
Procedure Premises(R) // Retrieve premises of R
Requires: true
Ensures: res = Prems(R)

In addition, we also give the specifications of two auxiliary procedures IsAxiomRule(R) and
IsSynthesisRule(R) which returns true if the rule R is an axiom rule or a synthesis rule.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:36

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

Procedure IsAxiomRule(R) // Check if R is an axiom rule
Requires: R ∈ { |−Π , ⊥1L , ⊥2L , U1Π , U2Π , U1Σ , U2Σ }
Ensures: (res = true) ∧ (Prems(R) = ∅)
Requires: R < { |−Π , ⊥1L , ⊥2L , U1Π , U2Π , U1Σ , U2Σ }
Ensures: res = false

The above specifications of IsAxiomRule(R) specify two possible cases of the input R, respectively
when R is an axiom rule (R ∈ { |−Π , ⊥1L , ⊥2L , U1Π , U2Π , U1Σ , U2Σ }), or otherwise. In the former case, we
can ensure that there are no premises in R (i.e., Prems(R) = ∅).
Procedure IsSynthesisRule(R) // Check if R is a synthesis rule
Requires: R ∈ {U1Π , U2Π , U1Σ , U2Σ , UIH }
Ensures: res = true
Requires: R < {U1Π , U2Π , U1Σ , U2Σ , UIH }
Ensures: (res = false) ∧ (Asms(R) = ∅)

The specifications of the procedure IsSynthesisRule denote two cases when R is a synthesis rule or
not. In the latter case, it is obvious that the assumption set of R is empty (i.e., Asms(R) = ∅).
In the following subsections, we illustrate the formal verification of the main proof search procedure
Prove in Figure 10 on its three specifications, depicted by pairs of Requires/Ensures. We perform a
Hoare-style forward verification, in which −→ is a weakening on program states.
The formal verification of other lemma synthesis procedures in Section 5, i.e., SynthesizeLemma,
RefineAnte, RefineConseq, Preprocess, and FineTuneConseq in Figures 11, 12, 14, 15, and 17 are
straightforward.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic
B.1

9:37

Verification of the first specification of the proof search procedure in Figure 10

Procedure Prove(H, L, F 1 |− F 2 , mode)
Requires: (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L)
Ensures: (res = (Unkn, ∅, ∅)) ∨ ∃ ξ , A. (res = (Valid⟨ξ ⟩, ∅, A) ∧ (valid(A) → valid ID (H, L, F 1 |−F 2 )))
Invariant: sound(R)
// { (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ sound(R) }
1: R ← {Unify(R, (H, L, F 1 |− F 2 )) | R ∈ R}
// { (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ sound(R) }
//sound(R) ∧ R ⊆ R → sound(R)
2: Lsyn ← ∅
// { (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅ ∧ sound(R) }
3: if mode = SynLM and NeedLemmas(F 1 |− F 2 , R) then
4:
Lsyn ← SynthesizeLemma(L, F 1 |− F 2 )
//unreachable code
R ← R ∪ {Unify(R, (H, Lsyn , F 1 |− F 2 )) | R ∈ {LML , LMR }}
5:
// { (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅ ∧ sound(R) }
6: for each R in R do
//sound(R) ∧ R ∈ R → sound(R)
// { (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅ ∧ sound(R) }
7:
A←∅
8:
if IsSynthesisRule(R) then A ← Assumptions(R)
// { (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅ ∧ sound(R) ∧ A = Asms(R) }
9:
if IsAxiomRule(R) then
// { . . . ∧ Lsyn = ∅ ∧ sound(R) ∧ Asms(R) = A ∧ Prems(R) = ∅ }
// −→ { Lsyn = ∅ ∧ (valid(A) → valid ID (H, L, F 1 |−F 2 )) }
//valid ID (∅) = true
10:
ξ ← CreateWitnessProofTree(F 1 |− F 2 , R, ∅)
11:
return (Valid⟨ξ ⟩, Lsyn , A)
// { Lsyn = ∅ ∧ (valid(A) → valid ID (H, L, F 1 |−F 2 )) ∧ res = (Valid⟨ξ ⟩, Lsyn , A) }
// −→ { ∃ ξ , A. (res = (Valid⟨ξ ⟩, ∅, A) ∧ (valid(A) → valid ID (H, L, F 1 |−F 2 ))) }
12:
(Hi , Li , F 1i |− F 2i )i = 1...n ← Premises(R)
// { (mode = NoSyn) ∧ hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅ ∧ sound(R)
n ∧ Ón (L = L) }
//
∧ Asms(R) = A ∧ Prems(R) = {Hi , Li , F 1i |− F 2i }i=1
i=1 i
i ,A )
13:
(r i , Lsyn
i i = 1...n ← Prove(Hi , L ∪ Lsyn ∪ Li , F 1i |− F 2i , mode)i = 1...n
Ó
// { . . . ∧ Lsyn = ∅ ∧ (valid(A) ∧ ni=1 valid ID (Hi , Li , F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
//
i=1 (Lsyn = ∅ ∧ ((r i = Unkn ∧ Ai = ∅)
//
∨ (hasU nk(F 1i |−F 2i ) ∧ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ (valid(Ai ) → valid ID (Hi , Li , F 1i |−F 2i )))))
//
∨ (¬hasU nk(F 1i |−F 2i ) ∧ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ Ai = ∅ ∧ valid ID (Hi , Li , F 1i |−F 2i ))))) }
Ó
// −→ { Lsyn = ∅ ∧ (valid(A) ∧ ni=1 valid ID (Hi , Li , F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
//
i=1 (Lsyn = ∅ ∧ ((r i = Unkn ∧ Ai = ∅)
//
∨ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ (valid(Ai ) → valid ID (Hi , Li , F 1i |−F 2i ))))) }
//valid(∅) = true
Fig. 20. Verification of the proof search procedure Prove on the first specification (Part 1)

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:38

14:

15:
16:

17:

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

Ó
// { Lsyn = ∅ ∧ (valid(A) ∧ ni=1 valid ID (Hi , Li , F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
//
i=1 (Lsyn = ∅ ∧ ((r i = Unkn ∧ Ai = ∅)
//
∨ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ (valid(Ai ) → valid ID (Hi , Li , F 1i |−F 2i ))))) }
if r i = Valid⟨ξ i ⟩ for all i = 1 . . . n then
Ó
// { Lsyn = ∅ ∧ (valid(A) ∧ ni=1 valid ID (Hi , Li , F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
|−
//
i=1 (r i = Valid⟨ξ i ⟩ ∧ Lsyn = ∅ ∧ (valid(Ai ) → valid ID (Hi , Li , F 1i F 2i ))) }
|
−
ξ ← CreateWitnessProofTree(F 1 F 2 , R, {ξ 1 , . . . , ξ n })
1 ∪ . . . ∪ Ln , A ∪ A ∪ . . . ∪ A )
return (Valid⟨ξ ⟩, Lsyn ∪ Lsyn
1
n
syn
Ó
// { Lsyn = ∅ ∧ (valid(A) ∧ ni=1 valid ID (Hi , Li , F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
|−
//
i=1 (Lsyn = ∅ ∧ (valid(Ai ) → valid ID (Hi , Li , F 1i F 2i )))
//
∧ res = (Valid⟨ξ ⟩, ∅, A ∪ A1 ∪ . . . ∪ An ) }
return (Unkn, ∅, ∅)
// { res = (Unkn, ∅, ∅) }
Fig. 21. Verification of the proof search procedure Prove on the first specification (Part 2)

Given the post-state after line 16 in Figure 21, we prove the postcondition of Prove as follows,
where −→ is a weakening on program states.
// the program state at line 16
Ó
Lsyn = ∅ ∧ (valid(A) ∧ ni=1 valid ID (Hi , Li , F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 ))
Ón
i
∧ i=1 (Lsyn
= ∅ ∧ (valid(Ai ) → valid ID (Hi , Li , F 1i |−F 2i )))
∧ res = (Valid⟨ξ
Ón ⟩, ∅, A ∪ A1 ∪ . . . ∪ An ) }
−→ (valid(A)
∧
i=1 valid ID (Hi , Li , F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 ))
Ó
∧ ni=1 (valid(Ai ) → valid ID (Hi , Li , F 1i |−F 2i ))
∧ res = (Valid⟨ξ ⟩, ∅, A ∪ A1 ∪ . . . ∪ An )
Ó
−→ (valid(A)∧ ni=1 valid(Ai ) → valid ID (H, L, F 1 |−F 2 )) ∧ res=(Valid⟨ξ ⟩, ∅, A∪A1 ∪ . . . ∪An )
−→ (valid(A∪A1 ∪ . . . ∪An ) → valid ID (H, L, F 1 |−F 2 )) ∧ res=(Valid⟨ξ ⟩, ∅, A∪A1 ∪ . . . ∪An )
−→ ∃ ξ , A. (res = (Valid⟨ξ ⟩, ∅, A) ∧ (valid(A) → valid ID (H, L, F 1 |−F 2 ))
−→ (res = (Unkn, ∅, ∅)) ∨ ∃ ξ , A. (res = (Valid⟨ξ ⟩, ∅, A) ∧ (valid(A) → valid ID (H, L, F 1 |−F 2 )))
// the post condition in the first specification of Prove

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic
B.2

9:39

Verification of the second specification of the proof search procedure in Figure 10

Procedure Prove(H, L, F 1 |− F 2 , mode)
Requires: (mode = NoSyn) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L)
Ensures: (res = (Unkn, ∅, ∅)) ∨ ∃ ξ . (res = (Valid⟨ξ ⟩, ∅, ∅) ∧ valid ID (H, L, F 1 |−F 2 ))
Invariant: sound(R)
1:

2:

3:
4:
5:

6:

7:

8:

9:

10:
11:

12:

13:

// { (mode = NoSyn) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ sound(R) }
R ← {Unify(R, (H, L, F 1 |− F 2 )) | R ∈ R}
//sound(R) ∧ R ⊆ R → sound(R)
// { (mode = NoSyn) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ sound(R)
//
∧ R ∩ {U1Π , U2Π , U1Σ , U2Σ , UIH } = ∅ }
//since ¬hasU nk(F 1 |−F 2 )
Lsyn ← ∅
// { (mode = NoSyn) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅
//
∧ sound(R) ∧ R ∩ {U1Π , U2Π , U1Σ , U2Σ , UIH } = ∅ }
if mode = SynLM and NeedLemmas(F 1 |− F 2 , R) then
//unreachable code
Lsyn ← SynthesizeLemma(L, F 1 |− F 2 )
R ← R ∪ {Unify(R, (H, Lsyn , F 1 |− F 2 )) | R ∈ {LML , LMR }}
// { (mode = NoSyn) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅
//
∧ sound(R) ∧ R ∩ {U1Π , U2Π , U1Σ , U2Σ , UIH } = ∅ }
for each R in R do
// { (mode = NoSyn) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅
//since R ∈ R
//
∧ sound(R) ∧ R < {U1Π , U2Π , U1Σ , U2Σ , UIH } }
A←∅
// { (mode = NoSyn) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅ ∧ A = ∅
//
∧ sound(R) ∧ R < {U1Π , U2Π , U1Σ , U2Σ , UIH } }
if IsSynthesisRule(R) then A ← Assumptions(R)
//unreachable since R is not a synthesis rule
// { . . .∧(mode = NoSyn)∧¬hasU nk(F 1 |−F 2 )∧valid(L)∧Lsyn = ∅∧A = ∅∧Asms(R) = ∅∧sound(R) }
//valid(∅)=true and valid ID (∅)=true
if IsAxiomRule(R) then
// { . . . ∧ Lsyn = ∅ ∧ A = ∅ ∧ Asms(R) = ∅ ∧ Prems(R) = ∅ ∧ valid ID (H, L, F 1 |−F 2 ) }
ξ ← CreateWitnessProofTree(F 1 |− F 2 , R, ∅)
return (Valid⟨ξ ⟩, Lsyn , A)
// { . . . ∧ Lsyn = ∅ ∧ A = ∅ ∧ valid ID (H, L, F 1 |−F 2 )) ∧ res = (Valid⟨ξ ⟩, Lsyn , A) }
// −→ { ∃ ξ . (res = (Valid⟨ξ ⟩, ∅, ∅) ∧ valid ID (H, L, F 1 |−F 2 )) }
(Hi , Li , F 1i |− F 2i )i = 1...n ← Premises(R)
Ó
// { . . . ∧ (mode = NoSyn) ∧ valid(L) ∧ Lsyn = ∅ ∧ A = ∅ ∧ ¬hasU nk(F 1 |−F 2 ) ∧ ni=1 (Li = L)
n ∧ sound(R) }
//
∧ Asms(R) = ∅ ∧ Prems(R) = {Hi , Li , F 1i |− F 2i }i=1
Ó
// −→
//since ¬hasU nk(F 1 |−F 2 ) → ni=1 (¬hasU nk(F 1i |−F 2i ))
Ón
// { (mode = NoSyn) ∧ valid(L) ∧ Lsyn = ∅ ∧ A = ∅ ∧ i=1 (¬hasU nk(F 1i |−F 2i ) ∧ Li = L)
n ∧ sound(R) }
//
∧ Asms(R) = ∅ ∧ Prems(R) = {Hi , Li , F 1i |− F 2i }i=1
i
(r i , Lsyn , Ai )i = 1...n ← Prove(Hi , L ∪ Lsyn ∪ Li , F 1i |− F 2i , mode)i = 1...n
Ó
// { . . . ∧ Lsyn = ∅ ∧ A = ∅ ∧ ( ni=1 valid ID (Hi , L, F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
|−
//
i=1 (((r i = Unkn) ∨ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ valid ID (Hi , L, F 1i F 2i )))) ∧ Lsyn =∅ ∧ Ai =∅) }
// −→
Ó
// { Lsyn = ∅ ∧ A = ∅ ∧ ( ni=1 valid ID (Hi , L, F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
|−
//
i=1 (((r i = Unkn) ∨ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ valid ID (Hi , L, F 1i F 2i )))) ∧ Lsyn =∅ ∧ Ai =∅) }
Fig. 22. Verification of the proof search procedure Prove on the second specification (Part 1)

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:40

14:

15:
16:

17:

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin

Ó
// { Lsyn = ∅ ∧ A = ∅ ∧ ( ni=1 valid ID (Hi , L, F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
|−
//
i=1 (((r i = Unkn) ∨ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ valid ID (Hi , L, F 1i F 2i )))) ∧ Lsyn =∅ ∧ Ai =∅) }
if r i = Valid⟨ξ i ⟩ for all i = 1 . . . n then
Ó
// { Lsyn = ∅ ∧ A = ∅ ∧ ( ni=1 valid ID (Hi , L, F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
|−
//
i=1 (r i = Valid⟨ξ i ⟩ ∧ valid ID (Hi , L, F 1i F 2i ) ∧ Lsyn =∅ ∧ Ai =∅) }
ξ ← CreateWitnessProofTree(F 1 |− F 2 , R, {ξ 1 , . . . , ξ n })
1 ∪ . . . ∪ Ln , A ∪ A ∪ . . . ∪ A )
return (Valid⟨ξ ⟩, Lsyn ∪ Lsyn
1
n
syn
Ó
// { . . . ∧ res = (Valid⟨ξ ⟩, ∅, ∅) ∧ ni=1 valid ID (Hi , L, F 1i |−F 2i ) ∧
Ó
// ( ni=1 valid ID (Hi , L, F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) }
// −→ { (res = (Valid⟨ξ ⟩, ∅, ∅) ∧ valid ID (H, L, F 1 |−F 2 ))) }
return (Unkn, ∅, ∅)
// { res = (Unkn, ∅, ∅) }
Fig. 23. Verification of the proof search procedure Prove on the second specification (Part 2)

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

Automated Lemma Synthesis in Symbolic-Heap Separation Logic
B.3

9:41

Verification of the third specification of the proof search procedure in Figure 10

Procedure Prove(H, L, F 1 |− F 2 , mode)
Requires: (mode = SynLM) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L)
Ensures: (res = (Unkn, ∅, ∅)) ∨ ∃ ξ , Lsyn .(res = (Valid⟨ξ ⟩, Lsyn , ∅) ∧ valid(Lsyn ) ∧ valid ID (H, L, F 1 |−F 2 ))
Invariant: sound(R)
// { (mode = SynLM) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ sound(R) }
1: R ← {Unify(R, (H, L, F 1 |− F 2 )) | R ∈ R}
// { (mode = SynLM) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ sound(R)
//sound(R) ∧ R ⊆ R → sound(R)
//since ¬hasU nk(F 1 |−F 2 )
//
∧ R ∩ {U1Π , U2Π , U1Σ , U2Σ , UIH } = ∅ }
2: Lsyn ← ∅
// { (mode = SynLM) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ Lsyn = ∅
//
∧ sound(R) ∧ R ∩ {U1Π , U2Π , U1Σ , U2Σ , UIH } = ∅ }
3: if mode = SynLM and NeedLemmas(F 1 |− F 2 , R) then
4:
Lsyn ← SynthesizeLemma(L, F 1 |− F 2 )
R ← R ∪ {Unify(R, (H, Lsyn , F 1 |− F 2 )) | R ∈ {LML , LMR }}
5:
// { (mode = SynLM) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ valid(Lsyn ) //w.r.t. the spec of SynthesizeLemma
//
∧ sound(R) ∧ R ∩ {U1Π , U2Π , U1Σ , U2Σ , UIH } = ∅ }
6: for each R in R do
// { (mode = SynLM) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ valid(Lsyn )
//
∧ sound(R) ∧ R < {U1Π , U2Π , U1Σ , U2Σ , UIH } }
//since R ∈ R
7:
A←∅
// { (mode = SynLM) ∧ ¬hasU nk(F 1 |−F 2 ) ∧ valid(L) ∧ valid(Lsyn ) ∧ A=∅
//
∧ sound(R) ∧ R < {U1Π , U2Π , U1Σ , U2Σ , UIH } }
8:
if IsSynthesisRule(R) then A ← Assumptions(R)
//unreachable since R is not a synthesis rule
|
// { . . .∧(mode = SynLM)∧¬hasU nk(F 1 −F 2 )∧valid(L)∧valid(Lsyn )∧A=∅∧Asms(R)=∅∧sound(R) }
9:
if IsAxiomRule(R) then
//valid(∅)=true and valid ID (∅)=true
// { . . . ∧ valid(Lsyn ) ∧ A = ∅ ∧ Asms(R) = ∅ ∧ Prems(R) = ∅ ∧ valid ID (H, L, F 1 |−F 2 ) }
10:
ξ ← CreateWitnessProofTree(F 1 |− F 2 , R, ∅)
11:
return (Valid⟨ξ ⟩, Lsyn , A)
// { . . . ∧ valid(Lsyn ) ∧ A = ∅ ∧ valid ID (H, L, F 1 |−F 2 ) ∧ res = (Valid⟨ξ ⟩, Lsyn , A) }
// −→ { ∃ ξ . (res = (Valid⟨ξ ⟩, Lsyn , ∅) ∧ valid(Lsyn ) ∧ valid ID (H, L, F 1 |−F 2 )) }
12:
(Hi , Li , F 1i |− F 2i )i = 1...n ← Premises(R)
Ó
// { . . . ∧ (mode = SynLM) ∧ valid(L) ∧ valid(Lsyn ) ∧ A = ∅ ∧ ¬hasU nk(F 1 |−F 2 ) ∧ ni=1 (Li = L)
n
//
∧ Asms(R) = ∅ ∧ Prems(R) = {Hi , Li , F 1i |− F 2i }i=1 ∧ sound(R) }
Ó
// −→
//since ¬hasU nk(F 1 |−F 2 ) → ni=1 (¬hasU nk(F 1i |−F 2i ))
Ón
// { (mode = SynLM) ∧ valid(L) ∧ valid(Lsyn ) ∧ A = ∅ ∧ i=1 (¬hasU nk(F 1i |−F 2i ) ∧ Li = L)
n ∧ sound(R) }
//
∧ Asms(R) = ∅ ∧ Prems(R) = {Hi , Li , F 1i |− F 2i }i=1
Fig. 24. Verification of the proof search procedure Prove on the third specification (Part 1)

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

9:42

13:

14:

15:
16:

17:

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin
Ó
// { (mode = SynLM) ∧ valid(L) ∧ valid(Lsyn ) ∧ A = ∅ ∧ ni=1 (¬hasU nk(F 1i |−F 2i ) ∧ Li = L)
n ∧ sound(R) }
//
∧ Asms(R) = ∅ ∧ Prems(R) = {Hi , Li , F 1i |− F 2i }i=1
i
(r i , Lsyn , Ai )i = 1...n ← Prove(Hi , L ∪ Lsyn ∪ Li , F 1i |− F 2i , mode)i = 1...n
Ó
// { . . . ∧ valid(Lsyn ) ∧ A = ∅ ∧ ( ni=1 valid ID (Hi , L, F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
//
i=1 ((r i = Unkn ∧ Lsyn = ∅ ∧ Ai = ∅)
i ) ∧ A = ∅))) }
//
∨ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ valid ID (Hi , L, F 1i |−F 2i ) ∧ valid(Lsyn
i
// −→
Ó
// { valid(Lsyn ) ∧ A = ∅ ∧ ( ni=1 valid ID (Hi , L, F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
//
i=1 ((r i = Unkn ∧ Lsyn = ∅ ∧ Ai = ∅)
i ) ∧ A = ∅))) }
//
∨ (∃ξ i . (r i = Valid⟨ξ i ⟩ ∧ valid ID (Hi , L, F 1i |−F 2i ) ∧ valid(Lsyn
i
Ón
|
−
// { valid(Lsyn ) ∧ A = ∅ ∧ ( i=1 valid ID (Hi , L, F 1i F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
//
i=1 ((r i = Unkn ∧ Lsyn = ∅ ∧ Ai = ∅)
if r i = Valid⟨ξ i ⟩ for all i = 1 . . . n then
Ó
// { valid(Lsyn ) ∧ A = ∅ ∧ ( ni=1 valid ID (Hi , L, F 1i |− F 2i ) → valid ID (H, L, F 1 |−F 2 )) ∧
Ón
i
|−
//
i=1 (r i = Valid⟨ξ i ⟩ ∧ valid(Lsyn ) ∧ Ai = ∅ ∧ valid ID (Hi , L, F 1i F 2i )) }
ξ ← CreateWitnessProofTree(F 1 |− F 2 , R, {ξ 1 , . . . , ξ n })
1 ∪ . . . ∪ Ln , A ∪ A ∪ . . . ∪ A )
return (Valid⟨ξ ⟩, Lsyn ∪ Lsyn
1
n
syn
Ón
1 ∪ . . . ∪ L n , ∅) ∧ valid(L
i
// { . . . ∧ res = (Valid⟨ξ ⟩, Lsyn ∪ Lsyn
syn ) ∧ i=1 valid(Lsyn ) ∧
syn
Ón
Ón
|
|
−
−
//
valid
(H
,
L,
F
F
)
}
∧
(
valid
(H
,
L,
F
F
)→valid
(H,
L,
F 1 |−F 2 ))
i
1i
2i
i
1i
2i
ID
ID
ID
i=1
i=1
1 ∪ . . . ∪ L n , ∅)
// −→ { res = (Valid⟨ξ ⟩, Lsyn ∪Lsyn
syn
1 ∪ . . . ∪ L n ) ∧ valid (H,L,F |−F ) }
//
∧ valid(Lsyn ∪ Lsyn
1 2
ID
syn

return (Unkn, ∅, ∅)
// { res = (Unkn, ∅, ∅) }
Fig. 25. Verification of the proof search procedure Prove on the third specification (Part 2)

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 9. Publication date: January 2018.

