Frame Inference for Inductive Entailment Proofs in Separation Logic
Abstract
Given separation logic formulae \(A\) and \(C\), frame inference is the problem of checking whether \(A\) entails \(C\) and simultaneously inferring residual heaps. Existing approaches on frame inference do not support inductive proofs with general inductive predicates. In this work, we present an automatic frame inference approach for an expressive fragment of separation logic. We further show how to strengthen the inferred frame through predicate normalization and arithmetic inference. We have integrated our approach into an existing verification system. The experimental results show that our approach helps to establish a number of nontrivial inductive proofs which are beyond the capability of all existing tools.
1 Introduction
In this work, we propose a sound approach for frame inference which aims to enhance modular verification in an expressive SL fragment with general inductive predicates and Presburger arithmetic. Intuitively, given an entailment \(\varDelta _a ~{\models }~ \varDelta _c\), our goal is to infer a satisfiable frame axiom \(\varDelta _f\) such that \(\varDelta _a ~{\models }~ \varDelta _c *\varDelta _f\) holds. Our approach works as follows. We first augment the entailment checking with an unknown secondorder variable \({\mathtt{{U_f}}}(\bar{t})\) as a placeholder of the frame, where \(\bar{t}\) is a set of pointertyped variables common in \(\varDelta _{a}\) and \(\varDelta _{c}\). That is, the entailment checking becomes \(\varDelta _a ~\models ~ \varDelta _c*{\mathtt{{U_f}}}(\bar{t})\). Afterwards, the following two steps are conducted. Firstly, we invoke a novel proof system to derive a cyclic proof for \(\varDelta _a ~\models ~ \varDelta _c *{\mathtt{{U_f}}}(\bar{t})\) whilst inferring a predicate which \({\mathtt{{U_f}}}\) must satisfy so that the entailment is valid. We show that the cyclic proof is valid if this predicate is satisfiable. Secondly, we strengthen the inferred frame with shape normalization and arithmetic inference.
For the first step, we design a new cyclic proof system (e.g., based on [2, 3]) with an automated cut rule so as to effectively infer the predicate on \({\mathtt{{U_f}}}\). A cyclic proof is a derivation tree whose root is the given entailment checking and whose edges are constructed by applying SL proof rules. A derivation tree of a cyclic proof may contain virtual backlinks, each of which links a (leaf) node back to an ancestor. Intuitively, a backlink from a node l to an internal node i means that the proof obligation at l is induced by that at i. Furthermore, to avoid potentially unsound cycles (i.e., selfcycles), a global soundness condition must be imposed upon these derivations to qualify them as genuine proofs. In this work, we develop a sequentbased cyclic proof system with a cyclic cut rule so as to form backlinks effectively and check the soundness condition eagerly. Furthermore, we show how to extract lemmas from the proven cyclic proofs and reuse them through lemma application for an efficient proof system. These synthesized lemmas work as dynamic cuts in the proposed proof system.
For the second step, we strengthen the inferred predicate on the frame \({\mathtt{{U_f}}}(\bar{t})\) so that it becomes more powerful in establishing correctness of certain programs. In particular, the inferred frame is strengthened with predicate normalization and arithmetic inference. The normalization includes predicate split (i.e., to expose the spatial separation of the inferred frame) and predicate equivalence (i.e., to relate the inferred frame with usersupplied predicates). The arithmetic inference discovers predicates on pure properties (size, sum, height, content and bag) to support programs which require induction reasoning on both shape and data properties.
Lastly, we have implemented the proposal and integrated it into a modular verification engine. Our experiments show that our approach infers strong frames which enhances the verification of heapmanipulating programs.
2 Preliminaries
In our framework, we may have lemmas to assist program verification. A lemma \(\iota \) of the form \(\varDelta _l ~{\rightarrow }~ \varDelta _r\), which means that the entailment \(\varDelta _l\,\models \,\varDelta _r\) holds. We write \(A\,{\leftrightarrow }\,B\), a short form of \(A\,{\rightarrow }\,B\) and \(B{\,\rightarrow }\,A\), to denote a twoway lemma. If \(A\,{\leftrightarrow }\,B\), \(A\) is semantically equivalent to \(B\). We use \(E\) and \(F\) to denote an entailment problem.
3 Illustrative Example
In the following, we first discuss the limitation of the existing entailment procedures [1, 8] to the frame inference problem. Given an entailment, these procedures deduce it until the following subgoal is obtained: Open image in new window . Then, they conclude that \(\varDelta _a\) is the residual frame. However, these approaches provide limited support for proofs of induction. While [1] provides inference rules as a sequence of inductive reasoning for hardwired lists and trees, our previous work [8] supports inductive proofs via usersupplied lemmas [30]. Hence, it is very hard for these procedures to automatically infer the frame for the entailments which require proofs of induction.
4 Frame Inference
In this section, we present our approach for frame inference in detail. Given an entailment \(\varDelta _a ~{{\vdash }}~ \varDelta _c\), where \(\varDelta _{a}\) is the antecedent (LHS) and \(\varDelta _{c}\) is the consequence (RHS), our system attempts to infer a frame \(\varDelta _{f}\) such that when a frame is successfully inferred, the validity of the entailment \(\varDelta _a ~{{\vdash }}~ \varDelta _c {*}\varDelta _f\) is established at the same time.
Our approach has three main steps. Firstly, we enrich RHS with an unknown predicate in the form of \({\mathtt{{{\mathtt{{U}}}}}}(\bar{v})\) to form the entailment \(\varDelta _a ~{\vdash }_{{L}}~ \varDelta _c{*}{\mathtt{{{\mathtt{{U}}}}}}(\bar{v})\) where \(\bar{v}\) includes all free pointertyped variables of \(\varDelta _a\) and \(\varDelta _c\) and \({L}\) is the union of a set of usersupplied lemmas and a set of induction hypotheses (initially \(\emptyset \)). Among these, the parameters are annotated with \({{{\scriptstyle \#}}}\) following the principle that instantiation (and subtraction) must be done before inference. The detail is as follows: (i) all common variables of \(\varDelta _a\) and \(\varDelta _c\) are \({{{\scriptstyle \#}}}\)annotated; (ii) pointsto pointers of \(\varDelta _c\) are \({{{\scriptstyle \#}}}\)annotated; (iii) the remaining pointers are not \({{{\scriptstyle \#}}}\)annotated. In the implementation, inference of frame predicates is performed incrementally such that shape predicates are inferred prior to pure ones. Secondly, we construct a proof of the entailment and infer a set of constraints \(\mathcal {R}\) for \({\mathtt{{{\mathtt{{U}}}}}}(\bar{v})\). Thirdly, we check the satisfiability of \(\mathcal {R}\) using the decision procedure in [25, 26].
Given an entailment check in the form of \(\varDelta _a\,{{\vdash }}_{{L}}\,\varDelta _c\), the rules shown in Fig. 3 are designed to subtract the heap (via the rules \([\underline{\mathbf{\scriptstyle M}}]\) and \([\underline{\mathbf{\scriptstyle PREDM}}]\)) on both sides until their heaps are empty. After that, it checks the validity for the implication of two pure formulas by using an SMT solver, like Z3 [27], as shown in rule \([\underline{\mathbf{\scriptstyle EMP}}]\). Algorithmically, this entailment checking is performed as follows.

Matching. The rules \([\underline{\mathbf{\scriptstyle M}}]\) and \([\underline{\mathbf{\scriptstyle PREDM}}]\) are used to match up identified heap chains. Starting from identified root pointers, the procedure keeps matching all their reachable heaps. It unifies corresponding fields of matched roots by using the following auxiliary function \(\text {freeEQ}(\rho )\): \(\text {freeEQ}([u_i/v_i]^n_{i=1}) = \bigwedge ^n_{i=1} \{ u_i = v_i \}\).

Unfolding. The rules \([\underline{\mathbf{\scriptstyle LU}}]\) and \([\underline{\mathbf{\scriptstyle RU}}]\) are used to derive alternative heap chains. While rule \([\underline{\mathbf{\scriptstyle LU}}]\) presents the unfolding in the antecedent, \([\underline{\mathbf{\scriptstyle RU}}]\) in the consequent.

Applying Lemma. Rule \([\underline{\mathbf{\scriptstyle CCUT}}]\) derives yet other alternative heap chains. For LHS which has at least one \(\mathtt {UD}\) predicate, we attempt to apply a lemma as an alternative search using \([\underline{\mathbf{\scriptstyle CCUT}}]\) rule. We notice that as we assume that a lemma which is supplied by the user is valid, applying this lemma does not requires the global condition.
Definition 1
(Preproof). A preproof of entailment \(E\) is a pair (\(\mathcal{T}_{i}\), \(\mathcal L\)) where \(\mathcal{T}_{i}\) is a derivation tree and \(\mathcal L\) is a backlink function such that: the root of \(\mathcal{T}_{i}\) is \(E\); for every edge from \(E_i\) to \(E_j\) in \(\mathcal{T}_{i}\), \(E_i\) is a conclusion of an inference rule with a premise \(E_{j}\). There is a backlink between \(E_c\) and \(E_l\) if there exists \(\mathcal L\)(\(E_l\)) = \(E_c\) (i.e., \(E_{c}=E_{l}\,\theta \) with some substitution \(\theta \)) ; and for every leaf \(E_l\), \(E_l\) is an axiom rule (without conclusion).
If \(\mathcal L\)(\(E_l\)) = \(E_c\), \(E_{l}\) (resp. \(E_{c}\)) is referred as a bud (resp. companion).
Definition 2

\(\alpha _{i{+}1}\) is the subformula containing an instance of \({\mathtt{{P}}}(\bar{t})\) in \(\varDelta _{a_{i+1}}\);

or \({\varDelta _{a_i} {{\vdash }_{{L}_i}} \varDelta _{c_i} }\) is the conclusion of an unfolding rule, \(\alpha _i\) is an instance predicate \({\mathtt{{P}}}(\bar{t})\) in \(\varDelta _{a_i}\) and \(\alpha _{i+1}\) is a subformula \(\varDelta \)[\(\bar{t}\)/\(\bar{v}\)] which is a definition rule of the inductive predicate \({\mathtt{{P}}}(\bar{v})\). i is a progressing point of the trace.
To ensure that a preproof is sound, a global soundness condition must be imposed to guarantee wellfoundedness.
Definition 3
(Cyclic proof). A preproof (\(\mathcal{T}_{i}\), \(\mathcal L\)) of \(\varDelta _{a}\,{{\vdash }_{{L}}}\,\varDelta _{c}\) is a cyclic proof if, for every infinite path \((\varDelta _{a_i}\,{{\vdash }_{{L}_i}}\,\varDelta _{c_i})_{i{\ge }0}\) of \(\mathcal{T}_{i}\), there is a tail of the path \(p{=}(\varDelta _{a_i}\,{{\vdash }_{{L}_i}}\,\varDelta _{c_i})_{i{\ge }n}\) such that there is a trace following p which has infinitely progressing points.
Brotherston et al. proved [2] that \(\varDelta _{a} ~{\vdash }~ \varDelta _{c}\) holds if there is a cyclic proof of \(\varDelta _{a} ~{{\vdash }}_{\emptyset }~ \varDelta _{c}\) where \(\varDelta _{a}\) and \(\varDelta _{c}\) do not contain any unknown predicate.
Frame Inference. The two inference rules shown in Fig. 4 are designed specifically to infer constraints for frame. In these rules, \({\bigtriangledown }(\bar{w},\pi )\) is an auxiliary function that existentially quantifies free variables in \(\pi \) that are not in the set \(\bar{w}\). This function extracts relevant arithmetic constraints to define data contents of the unknown predicates. \(\mathtt{R}(r{,}\bar{t})\) is either \(r{\mapsto }c(\bar{t})\) or a known (defined) predicate \({\mathtt{{P}}}(r{,}\bar{t})\), or an unknown predicate \({\mathtt{{U'}}}(r{,}\bar{t}{,}\bar{w}{{{\scriptstyle \#}}})\). The # in the unknown predicates is used to guide inference and proof search. We only infer on pointers without \({{{\scriptstyle \#}}}\)annotation. \({\mathtt{{{\mathtt{{U}}}_{f}}}}(\bar{w},\bar{t'})\) is another unknown predicate which is generated to infer the shape of pointers \(\bar{w}\). Inferred pointers are annotated with \({{{\scriptstyle \#}}}\) to avoid double inference. A new unknown predicate \(\mathtt {{\mathtt{{U}}}_{f}}\) is generated only if there exists at least one parameter not to be annotated with \({{{\scriptstyle \#}}}\) (i.e., \(\bar{w}\cup \bar{t'} {\ne } \emptyset \)). To avoid conflict between the inference rules and the other rules (e.g., unfolding and matching), root pointers of a heap formula must be annotated with \({{{\scriptstyle \#}}}\) in unknown predicates. For example, in our system while Open image in new window is legal, \(x{\mapsto }{\mathtt{{c_1}}}(y){*}{\mathtt{{U_1}}}(x,y)\) is illegal. Our system applies subtraction on the heap pointed to by \(x\) rather than inference for the following check: Open image in new window .
Soundness. The soundness of the inference rules in Fig. 3 has been shown in unfoldandmatch systems for general inductive predicates [3, 8]. In the following, we present the soundness of the inference rules in Fig. 4. We introduce the notation \(\mathcal{R}(\varGamma )\) to denote a set of predicate definitions \(\varGamma {\,=\,}\{{\mathtt{{U}}}_1(\bar{v}_1)\,{\equiv }\,\varPhi _1,..{\mathtt{{U}}}_n(\bar{v}_n)\,{\equiv }\,\varPhi _n\}\) satisfying the set of constraints \(\mathcal{R}\). That is, for all constraints \({\varDelta _l\Rightarrow \varDelta _r}\in \mathcal{R}\), (i) \(\varGamma \) contains states (\(s_i\), \(h_i\)), a predicate definition for each unknown predicate appearing in \(\varDelta _l\) and \(\varDelta _r\); (ii) by interpreting all unknown predicates according to \(\varGamma \), then it is provable that \(\varDelta _l\) implies \(\varDelta _r\) (i.e., there exists \(s_i \subseteq s\), \(h_i \subseteq h\) for \(i \in \{1..n\}\), and \(s, h\,\models \,\varDelta _l\) implies \(s, h\models \varDelta _r\)), written as Open image in new window .
Lemma 1
Given the entailment judgement \( \varDelta _{a}~{\vdash _{\{\}}}~\varDelta _{c}\,{\leadsto }\,\mathcal {R} \), if there is \({\varGamma }\) such that \(\mathcal{R}(\varGamma )\), the entailment \({\varGamma }{:} \varDelta _{a}{{\vdash }} \varDelta _{c}\) holds.
The soundness of the predicate synthesis requires that if definitions generated for unknown predicates are satisfiable, then the entailment is valid.
Theorem 1
Given the entailment judgement \(\varDelta _{a}\,{\vdash }_{\emptyset }\,\varDelta _{c} {\leadsto } \mathcal {R}\) \(\varDelta _a(\varGamma )\,{{\vdash }}\,\varDelta _c(\varGamma )\) holds if there exists a solution \(\varGamma \) of \(\mathcal {R}\).
Theorem 1 follows from the soundness of the rules in Fig. 3 and Lemma 1.
5 Extensions
In this section, we present two ways to strengthen the inferred frame, by inferring pure properties and by normalizing inductive predicates.
Pure Constraint Inference. The inferred frame is strengthened with pure constraints following two phases. We first enrich the shapebase frame with pure properties such as size, height, sum, set of addresses/values, and their combinations. After that, we apply the same three steps in Sect. 4 to infer relational assumptions on the new pure properties. Lastly, we check satisfiability of these assumptions using FixCalc [34].
Normalization. We aim to relate the inferred frame to existing userprovided predicates if possible as well as to explicate the heap separation (a.k.a. pointer nonaliasing) which may be implicitly constrained through predicates. Particularly, we present a lemma synthesis mechanism to explore relations between inductive predicates. Our system processes each inductive predicate in four steps. First, it generates heaponly conjectures (with quantifiers). Secondly, it enriches these conjectures with unknown predicates. Thirdly, it invokes the proposed entailment procedure to prove these conjectures, infer definitions for the unknown predicates and synthesize the lemmas. Last, it strengthens the inferred lemma with pure inference.
In the following, we present two types of normalization. This first type is to generate equivalence lemmas. This normalization equivalently matches a new generated predicate to an existing predicate in a given predicate library. Under the assumption that a library of predicates is provided together with advanced knowledge (i.e., lemmas in [1]) to enhance completeness. This normalization helps to reuse this knowledge for the new synthesized predicates, and potentially enhance the completeness of the proof system. Intuitively, given a set \(\mathtt {S}\) of inductive predicates and another inductive predicate \(\mathtt {P}\) (which is not in \(\mathtt {S}\)), we identify all predicates in \(\mathtt {S}\) which are equivalent to \(\mathtt {P}\). Heaponly conjecture is generated to explore the equivalent relation between two predicates, e.g., in the case of \({\mathtt{{P}}}(x,\bar{v})\) and \({\mathtt{{Q}}}(x,\bar{w})\): \(\forall \bar{v} {\cdot } {\mathtt{{P}}}(\mathtt{root},\bar{v}) {\rightarrow } {\exists } \bar{w}{\cdot } {\mathtt{{Q}}}(\mathtt{root},\bar{w}) \). The shared root parameter \(x\) has been identified by examining all permutations of root parameters of the two predicates. Moreover, our system synthesizes lemmas incrementally for the combined domains of shape and pure properties. For example, with \(\mathtt {lln}\) and \(\mathtt {lsegn}\), our system generates the following lemma afterwards: \({\mathtt{{lsegn}}}(\mathtt{root}{,}\mathtt{null}{,}n) {\leftrightarrow } {\mathtt{{lln}}}(\mathtt{root}{,}n)\).
6 Implementation and Experiments
Inductive entailment checks
Entailment Proving. In Table 1, we evaluate \(\mathtt {S2ENT}\) on a set of 36 valid entailment problems that require induction reasoning techniques. In particular, Ent 1–5 were taken from Smallfoot [1], Ent 6–19 from Open image in new window [3, 5], Ent 20–28 from [9], and Ent 29–36 were generated by us. We evaluate \(\mathtt {S2ENT}\) against the existing proof systems presented for userdefined predicates. While the tools reported in [8, 12, 36] could handle a subset of these benchmarks if users provide auxiliary lemmas/axioms, [15] was designed neither for those inductive predicates in Ent 6–28 nor frame problems in Ent 29–36. The only two tools which we can compare \(\mathtt {S2ENT}\) with are Open image in new window [3] and \(\mathtt {songbird}\) [40].
The experimental results are presented in Table 1. The second column shows the entailment problems. Column \(bl\) captures the number of backlinks in cyclic proofs generated by \(\mathtt {S2ENT}\). We observe that most of problems require only one backlink in the cyclic proofs, except that Ent 4 requires two backlinks and Ent 13–15 of mutual inductive oddeven singly linked lists require three backlinks. The last three columns show the results of Open image in new window , \(\mathtt {songbird}\) and \(\mathtt {S2ENT}\) respectively. Each cell shown in these columns is either CPU times (in seconds) if the tool proves successfully, or TO if the tool runs longer than 30 s, or X if the tool returns a false positive, or NA if the entailment is beyond the capability of the tool. In summary, out of the 36 problems, Open image in new window solves 18 (with one TO  Ent 4); \(\mathtt {songbird}\) solves 25 (with two false positive  Ent 17 and 27 and one TO  Ent 23); and \(\mathtt {S2ENT}\) solves all 36 problems.
In Table 1, each entailment check in Ent 1–19 has \(\mathtt{emp}\) as frame axioms (their LHS and RHS have the same heaps). Hence, they may be handled by existing inductive proof systems like [3, 9, 15, 40]. In particular, Ent 1–19 include shapeonly predicates. The results show that Open image in new window and \(\mathtt {songbird}\) ran a bit faster than \(\mathtt {S2ENT}\) in most of the their successful cases. It is expected as \(\mathtt {S2ENT}\) requires additional steps for frame inference. Each entailment check in Ent 20–28 includes inductive predicates with pure properties (e.g., size and sortedness). While Open image in new window can provide inductive reasoning for arithmetic and heap domains separately [5], there is no system proposed for cyclic proofs in the combined domain. Hence, these problems are beyond the capability of Open image in new window . Ent 20 which requires mutual induction reasoning is the motivating example of \(\mathtt {songbird}\) (agumented with size property) [40]. In particular, \(\mathtt {sortll}\) represents a sorted list with smallest value \(\mathtt {min}\), and tll is a binary tree whose nodes point to their parents and leaves are linked by a linked list [19, 24]. \(\mathtt {S2ENT}\) solves each entailment incrementally: shapebased frame and then pure properties. The results show that \(\mathtt {S2ENT}\) was more effective and efficient than \(\mathtt {songbird}\).
Experiments on Glib library
LOC  #Pr  wo.  w.  

#\(\surd \)  Sec.  #syn  #\(\surd \)  Sec.  
gslist.c  698  52  41  8.93  126  47  12.47 
glist.c  784  51  39  19.41  132  46  30.01 
gtree.c  1204  40  36  57.31  96  36  60.88 
gnode.c  1128  65  52  37.78  174  53  53.40 
Modular Verification for Memory Safety. We enhance the existing program verifier \(\mathtt {S2}\) [24] with \(\mathtt {S2ENT}\) to automatically verify a range of heapmanipulating programs. We evaluate the enhanced \(\mathtt {S2}\) on the C library Glib open source [16] which includes nonGUI code from the GTK+ toolkit and the GNOME desktop environment. We conduct experiments on heapmanipulating files, i.e., singlylinked lists (gslist.c), doublylinked lists (glist.c), balanced binary trees (gtree.c) and Nary trees (gnode.c). These files contain fairly complex algorithms (e.g., sortedness) and the data structures used in gtree.c and gnode.c are very complex. Some procedures of gslist.c and glist.c were evaluated by tools presented in [9, 31, 36] where the user had to manually provide a large number of lemmas to support the tool. Furthermore, the verification in [9] is semiautomatic, i.e., verification conditions were manually generated. Besides the tool in [9], tools in [31, 36] were no longer available for comparison.
In Table 2 we show, for each file the number of lines of code (excluding comments) LOC and the number of procedures #Pr. We remark that these procedures include tailrecursive procedures which are translated from loops. The columns (\(\#\surd \)) (and sec.) show the number of procedures (and time in seconds) for which \(\mathtt {S2}\) can verify memory safety without (wo.) and with (w.) \(\mathtt {S2ENT}\). Column #syn shows the number of synthesized lemmas that used the technique in Sect. 5. With the lemma synthesis, the number of procedures that can be successfully verified increases from 168 (81%) to 182 (88%) with a time overhead of 28% (157 s/123 s).
A closer look shows that with \(\mathtt {S2ENT}\) we are able to verify a number of challenging methods in gslist.c and glist.c. By generating separating lemmas, \(\mathtt {S2ENT}\) successfully infers shape specifications of methods manipulating the last element of lists (i.e., \(\mathtt {g\_slist\_concat}\) in \(\mathtt {gslist.c}\) and \(\mathtt {g\_list\_append}\) in \(\mathtt {glist.c}\)). By generating equivalence lemmas, matching a newlyinferred inductive predicate with predefined predicates in \(\mathtt {S2}\) is now extended beyond the shapeonly domain. Moreover, the experimental results also show that the enhanced \(\mathtt {S2}\) were able to verify 41/52 procedures in gslist.c and 39/51 procedures in glist.c. In comparison, while the tool in [9] could semiautomatically verify 11 procedures in gslist.c and 6 procedures in glist.c, with usersupplied lemmas the tool in [31] could verify 22 procedures in gslist.c and 10 procedures in glist.c.
7 Related Work and Conclusion
This work is related to three groups of work. The first group are those on entailment procedures in SL. Initial proof systems in SL mainly focus on a decidable fragment combining linked lists (and trees) [1, 7, 11, 13, 14, 17, 22, 29, 32, 33]. Recently, Iosif et al. extend the decidable fragment to restricted inductive predicates [19]. Timos et al. [42] present a comprehensive summary on computational complexity for entailments in SL with inductive predicates. Smallfoot [1] and GRASShopper [33] provide systematic approaches for frame inference but with limited support for (general) inductive predicates. Extending these approaches to support general inductive predicates is nontrivial. GRASShopper is limited to a GRASSreducible class of inductive predicates. While Smallfoot system has been designed to allow the use of general inductive predicates, the inference rules in Smallfoot are hardwired for list predicates only and a set of new rules must be developed for a proof system targeting general inductive predicates. SLEEK [8] and jStar [12] support frame inference with a soundness guarantee for general inductive predicates. However, they provide limited support for induction using usersupplied lemmas [12, 30]. Our work, like [8, 36], targets an undecidable SL fragment including (arbitrary) inductive predicates and numerical constraints; we trade completeness for expressiveness. In addition to what are supported in [8, 36], we support frame inference with inductive reasoning in SL by providing a system of cyclic proofs.
The second group is work on inductive reasoning. Lemmas are used to enhance the inductive reasoning of heapbased programs [5, 12, 30]. They are used as alternative unfoldings beyond predicates’ definitions [5, 30], external inference rules [12], or intelligent generalization to support inductive reasoning [3]. Unfortunately, the mechanisms in these systems require users to supply those additional lemmas that might be needed during a proof. SPEN [15] synthesizes lemmas to enhance inductive reasoning for some inductive predicates with bags of values. However, it is designed to support some specific classes of inductive predicates and it is difficult to extend it to cater for general inductive predicates. For a solution to inductive reasoning in SL, Smallfoot [1, 3, 5] presents subtraction rules that are consequent from a set of lemmas of lists and trees. Brotherston et al. propose cyclic proof system for the entailment problem [2, 3]. Similarly, the circularity rule has been introduced in matching logic [38], Constraint Logic Programming [9] and separation logic combined with predicate definitions and arithmetic [40]. Furthermore, work in [39] supports frame inference based on an adhoc mechanism, using a simple unfolding and matching. Like [3, 9, 40], our system also uses historical sequents at case split steps as induction hypotheses. Beyond these systems [3, 9, 15, 40], \(\mathtt {S2ENT}\) infers frames for inductive proofs systematically; and thus it gives a better support for modular verification of heapmanipulating programs. Moreover, we show how we can incrementally support inductive reasoning for the combination of heap and pure domains. In contrast, there are no formalized discussions in [5, 9, 40] about inductive reasoning for the combined domains; while [5] supports these domains separately, [9, 40] only demonstrates their support through experimental results.
The third group is on lemma synthesis. In inductive reasoning, auxiliary lemmas are generated to discover theorems (e.g. [10, 23, 28]). The key elements of these techniques are heuristics used to generate equivalent lemmas for sets of given functions, constants and datatypes. In our work, we introduce lemma synthesis to strengthen the inductive constraints. To support theorem discovery, we synthesize equivalent and separating lemmas. This mechanism can be extended to other heuristics to enhance the completeness of modular verification.
Conclusion. We have presented a novel approach to frame inference for inductive entailments in SL with inductive predicates and arithmetic. The core of our proposal is the system of lemma synthesis through cyclic proofs in which backlinks are formed using the cut rule. Moreover, we have presented two extensions to strengthen the inferred frames. Our evaluation indicates that our system is able to infer frame axioms for inductive entailment checking that are beyond the capability of the existing systems.
Footnotes
 1.
In implementation, we add Open image in new window annotation into instantiated variables and nonheap variables to guide proof search which are not shown here.
Notes
Acknowledgements
This research is partially supported by project T2MOE1704 from Ministry of Education, Singapore.
References
 1.Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005). https://doi.org/10.1007/11575467_5CrossRefGoogle Scholar
 2.Brotherston, J.: Cyclic proofs for firstorder logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78–92. Springer, Heidelberg (2005). https://doi.org/10.1007/11554554_8CrossRefzbMATHGoogle Scholar
 3.Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bjørner, N., SofronieStokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 131–146. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642224386_12CrossRefzbMATHGoogle Scholar
 4.Brotherston, J., Fuhs, C., Gorogiannis, N., Pérez, J.N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of CSLLICS (2014)Google Scholar
 5.Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 350–367. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642351822_25CrossRefGoogle Scholar
 6.Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of biabduction. In: Proceedings of the 36th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 289–300. ACM (2009)Google Scholar
 7.Chen, T., Song, F., Wu, Z.: Tractability of separation logic with inductive definitions: beyond lists. In: Meyer, R., Nestmann, U. (eds.) 28th International Conference on Concurrency Theory (CONCUR 2017), vol. 85, pp. 37:1–37:17 (2017)Google Scholar
 8.Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via userdefined predicates in separation logic. SCP 77(9), 1006–1036 (2012)zbMATHGoogle Scholar
 9.Chu, D.H., Jaffar, J., Trinh, M.T.: Automatic induction proofs of datastructures in imperative programs. In: PLDI 2015 (2015)Google Scholar
 10.Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392–406. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642385742_27CrossRefGoogle Scholar
 11.Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 235–249. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642232176_16CrossRefGoogle Scholar
 12.Distefano, D., Parkinson, M.: jStar: towards practical verification for java. In: OOPSLA 2008, pp. 213–226. ACM, New York (2008)CrossRefGoogle Scholar
 13.Enea, C., Lengál, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 314–333. Springer, Cham (2014). https://doi.org/10.1007/9783319127361_17CrossRefGoogle Scholar
 14.Enea, C., Lengál, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. Formal Meth. Syst. Des. 51(3), 575–607 (2017)CrossRefGoogle Scholar
 15.Enea, C., Sighireanu, M., Wu, Z.: On automated lemma generation for separation logic with inductive definitions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 80–96. Springer, Cham (2015). https://doi.org/10.1007/9783319249537_7CrossRefzbMATHGoogle Scholar
 16.Glib. version 2.38.2 (2013). https://developer.gnome.org/glib/. Accessed 13 Oct 2017
 17.Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 532–549. Springer, Cham (2016). https://doi.org/10.1007/9783319402291_36CrossRefGoogle Scholar
 18.Holik, L., Lengál, O., Rogalewicz, A., Šimáček, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 740–755. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642397998_52CrossRefGoogle Scholar
 19.Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 21–38. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642385742_2CrossRefGoogle Scholar
 20.Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL, London, pp. 14–26, January 2001CrossRefGoogle Scholar
 21.Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642203985_4CrossRefGoogle Scholar
 22.Jansen, C., Katelaan, J., Matheja, C., Noll, T., Zuleger, F.: Unified reasoning about robustness properties of symbolicheap separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 611–638. Springer, Heidelberg (2017). https://doi.org/10.1007/9783662544341_23CrossRefGoogle Scholar
 23.Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J. Autom. Reason. 47(3), 251–289 (2011)MathSciNetCrossRefGoogle Scholar
 24.Le, Q.L., Gherghina, C., Qin, S., Chin, W.N.: Shape analysis via secondorder biabduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52–68. Springer, Cham (2014). https://doi.org/10.1007/9783319088679_4CrossRefGoogle Scholar
 25.Le, Q.L., Sun, J., Chin, W.N.: Satisfiability modulo heapbased programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382–404. Springer, Cham (2016). https://doi.org/10.1007/9783319415284_21CrossRefGoogle Scholar
 26.Le, Q.L., Tatsuta, M., Sun, J., Chin, W.N.: A decidable fragment in separation logic with inductive predicates and arithmetic. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 495–517. Springer, Cham (2017). https://doi.org/10.1007/9783319633909_26CrossRefGoogle Scholar
 27.de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540788003_24CrossRefGoogle Scholar
 28.McCasland, R., Bundy, A., Serge, A.: Automated discovery of inductive theorems. Stud. Logic Grammar Rhetor. 10(23), 135–149 (2007)Google Scholar
 29.Navarro Pérez, J.A., Rybalchenko, A.: Separation logic modulo theories. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 90–106. Springer, Cham (2013). https://doi.org/10.1007/9783319035420_7CrossRefGoogle Scholar
 30.Nguyen, H.H., Chin, W.N.: Enhancing program verification with lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 355–369. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540705451_34CrossRefGoogle Scholar
 31.Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 440–451. ACM, New York (2014)Google Scholar
 32.Pérez, J.A.N., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI, pp. 556–566 (2011)Google Scholar
 33.Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773–789. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642397998_54CrossRefGoogle Scholar
 34.Popeea, C., Chin, W.N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331–345. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540775058_26CrossRefGoogle Scholar
 35.Qin, S., He, G., Chin, W.N., Craciun, F., He, M., Ming, Z.: Automated specification inference in a combined domain via userdefined predicates. Sci. Comput. Program. 148(C), 189–212 (2017)CrossRefGoogle Scholar
 36.Qiu, X., Garg, P., Ştefănescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI, pp. 231–242. ACM, New York (2013)CrossRefGoogle Scholar
 37.Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, pp. 55–74. IEEE Computer Society, Washington, DC (2002)Google Scholar
 38.Rosu, G., Stefanescu, A.: Checking reachability using matching logic. In: OOPSLA 2012, pp. 555–574. ACM, New York (2012)Google Scholar
 39.Rowe, R.N.S., Brotherston, J.: Automatic cyclic termination proofs for recursive procedures in separation logic. In: CPP (2017)Google Scholar
 40.Ta, Q.T., Le, T.C., Khoo, S.C., Chin, W.N.: Automated mutual explicit induction proof in separation logic. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 659–676. Springer, Cham (2016). https://doi.org/10.1007/9783319489896_40CrossRefGoogle Scholar
 41.Tatsuta, M., Le, Q.L., Chin, W.N.: Decision procedure for separation logic with inductive definitions and Presburger arithmetic. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 423–443. Springer, Cham (2016). https://doi.org/10.1007/9783319479583_22CrossRefzbMATHGoogle Scholar
 42.Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 411–425. Springer, Heidelberg (2014). https://doi.org/10.1007/9783642548307_27CrossRefzbMATHGoogle Scholar
 43.Trinh, M.T., Le, Q.L., David, C., Chin, W.N.: Biabduction with pure properties for specification inference. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 107–123. Springer, Cham (2013). https://doi.org/10.1007/9783319035420_8CrossRefGoogle Scholar
 44.Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540705451_36CrossRefGoogle Scholar
Copyright information
<SimplePara><Emphasis Type="Bold">Open Access</Emphasis> This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.</SimplePara> <SimplePara>The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.</SimplePara>