Enhancing Symbolic Execution of Heap-based Programswith Separation Logic for Test Input Generation
Long H. Pham1 , Quang Loc Le2 , Quoc-Sang Phan3 , Jun Sun4 , and Shengchao Qin2
1

2Singapore University of Technology and Design
School of Computing & Digital Technologies, Teesside University, UK
3
Synopsys, Inc., USA
4Singapore Management University

Abstract. Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numeric domains,
existing symbolic execution techniques for heap-based programs are limited dueto the lack of a succinct and precise description for symbolic values over unbounded heaps. In this work, we present a new symbolic execution method forheap-based programs based on separation logic. The essence of our proposal iscontext-sensitive lazy initialization, a novel approach for efficient test input generation. Our approach differs from existing approaches in two ways. Firstly, ourapproach is based on separation logic, which allows us to precisely capture preconditions of heap-based programs so that we avoid generating invalid test inputs.
Secondly, we generate only fully initialized test inputs, which are more usefulin practice compared to those partially initialized test inputs generated by thestate-of-the-art tools. We have implemented our approach as a tool, called Java
StarFinder, and evaluated it on a set of programs with complex heap inputs. The
results show that our approach significantly reduces the number of invalid test
inputs and improves the test coverage.

1

Introduction

Symbolic execution [22] is getting momentum thanks to its capability of discovering
deep bugs. It is increasingly used not only in academic settings but also in industry,
such as in Microsoft, NASA, IBM and Fujitsu [11]. Despite having achieved tremendous success, symbolic execution has limited impact on testing programs with inputs
in the form of complex heap-based data structures (a.k.a. heap-based programs). The
dominant approach to symbolic execution of heap-based programs is lazy initialization [21], which postpones the initialization of reference variables and fields until they
are accessed (either assigned to or de-referenced). However, lazy initialization makes
no assumption on the shape of the input data structure, and explicitly enumerates all
possible heap objects that may bind to the input. This approach has the following fundamental limitations. Firstly, due to the lack of a succinct and precise description of
the shape of the input data structures, they often generate a large number of invalid test
inputs. Secondly, due to the enumeration of all possible heap objects that may bind to
the input, they often worsen the path explosion problem of symbolic execution. Lastly,
due to lazy initialization, the generated test inputs may be partially initialized (if somefields are never accessed) and need to be further concretized.

In the context of logic-based verification, the problem of specifying and reasoning
about heap-based programs has been studied for nearly five decades. The dominant approaches are based on separation logic [20, 32]. The strength of separation logic lies
in its separating conjunction ∗, which splits the heap into disjoint regions or heaplets.
This enables local reasoning, i.e., specification and reasoning are kept confined within
heaplets, independent of the rest of the heap. This is in contrast to global reasoning,i.e., the specification describes properties of the global heap, which “suffers from either limited applicability or extreme complexity, and scales poorly to programs of evenmoderate size” [32].
Surprisingly, there has been limited effort on using separation logic to enhance symbolic execution for test input generation. In this work, we start filling this gap. Firstly,
we propose a novel method for symbolic execution of heap-based programs based on
separation logic. In particular, we adopt a logic that combines separation logic with existentially quantified variables, inductive predicates and arithmetic which allows us toencode path conditions effectively in heap-based programs. Secondly, we enhance ourmethod with context-sensitive lazy initialization, i.e., we use preconditions written in
separation logic to guide the search, and only explore the states that are reachable when
the input satisfies the preconditions. As a result, all generated test inputs are valid.
In summary, we make the following main contributions.
1. We develop a symbolic execution engine for heap-based programs based on separation logic.
2. For efficiency, we present context-sensitive lazy initialization with a least fixed point
analysis to generate valid test inputs during symbolic execution.
3. We have implemented the proposed approach as a tool, called Java StarFinder5 , built
on top of Symbolic PathFinder [31], to generate test inputs for Java bytecode.
4. We have evaluated our tool on a set of Java programs including complex and mutabledata structures. All generated test inputs are valid and we achieve 98.98% branchcoverage on average.
The rest of this paper is organized as follows. Section 2 presents some backgroundand illustrates our proposal via an example. Section 3 describes the syntax of our corelanguage and its operational semantics. Our first contribution, a symbolic execution engine based on separation logic, is presented in Section 4. Our second contribution, thecontext-sensitive lazy initialization, is shown in Section 5. We present our implementation and evaluation in Section 6. Section 7 presents related work. Finally, we conclude
and discuss future works in Section 8.

2

Motivation and Illustration

In the following, we illustrate how our approach works with an example. Consider aprogram that represents a big non-negative integer in the form of a singly linked list,
i.e., each node of the lists contains a single digit of the number. Suppose we want togenerate test inputs for the method add shown in Fig. 1, which computes the sum of
two numbers in this representation.
5

https://github.com/star-finder/jpf-star

1
3
5
7

node add(node x, node y) {node dummyHead = new node(0, null); node z = dummyHead;while (x != null) {z.next = new node(x.val + y.val, null);x = x.next; y = y.next; z = z.next;}
return dummyHead.next;}

Fig. 1. Adding two numbers represented by linked lists

This method is designed to take two parameters x and y satisfying the following
preconditions: (1) all the digits of x and y are less than 5, and thus there is no carry; (2)x and y have the same number of digits. Condition (1) is a simple numerical constraint
which can be handled by existing symbolic execution engines. We thus leave it out ofthe discussion for the sake of simplicity. To capture condition (2), we define an inductive
predicate pre based on our fragment of separation logic as follows.
pred pre(a, b) ≡ (emp ∧ a = null ∧ b = null)∨ (∃n1 , n2 .a7→node( , n1 ) ∗ b7→node( , n2 ) ∗ pre(n1 , n2 ))Predicate emp means the heap is empty; predicate a7→node( , n1 ) states a points toan allocated object; and ∗ is the separation operator in separation logic. The data typenode corresponds to the class node in the program, which has two instance fields: val
containing the digit, and next referencing to another node object. The wildcard “ ” isused to indicate a “don’t care” value.
Intuitively, a linked list is recursively defined as a head points-to predicate with its
next field pointing to a sublist. In the base case of the definition, the heap is empty,
and both parameters a and b are null. In the recursive case, a7→node( , n1 ) signifies
that a points to an allocated object composed of a certain value (represented by “ ”)
and its next field n1 . Similarly, b points to an allocated object with its next field n2 .
Furthermore, n1 and n2 , i.e., the sublists of a and b respectively, satisfy pre as well.
In this definition, the separating conjunction operator ∗ splits the global heap into
three heaplets. The first two heaplets contain the node objects referenced respectively
by a and b, and the third one contains the sublists. This separation enforces that a andb refer to two distinct objects and their sublists are disjoint too. Since a and b must beeither both null or both not null, and likewise for the objects in their sublists, a andb have the same length.
To generate test inputs, we perform symbolic execution of method add(x, y) withprecondition pre(x,y). In the proposed symbolic execution, path conditions are formulae in the fragment of separation logic with inductive predicates and arithmetic. Reference variables are initialized by values obtained from a procedure, called enum. Initially,x and y are initialized to symbolic (stack) values X and Y respectively, and the pathcondition ∆ is initialized to pre(X,Y ). When variable x is first accessed at line 3, ourengine, through procedure enum, examines precondition pre(X,Y )6 for possible heap6

In all path conditions in this example we only show the constraints over those variables which
are relevant to the inputs x and y; the constraints over local variables z and dummyHead areseparated from x, y and thus are omitted for simplicity.

values for x. Procedure enum gets possible values through the least fixed point analysis
with procedure LFP. Procedure LFP unfolds predicate pre until the set of values reaches
a fixed point. In this example, procedure LFP only needs to unfold predicate pre onceand reach fixed point with two formulae corresponding to the two disjuncts in the definition of predicate pre. Then the engine substitutes the predicate pre(X,Y ) in the ∆ bythese two formulae (with α-renaming, i.e., substitutions of formal/actual parameters andof bound variables to avoid name collisions) to obtain two non-deterministic choices,and symbolic execution case splits. It first explores the path corresponding to the basecase and hence the constraint over X and Y in ∆ becomes X=null ∧ Y =null. We
use the constraint solver S2SATSL [24, 35, 26] to check that ∆ is satisfiable. There is nofurther case splitting in this path, and we have a test input where x and y are both null.
After exploring the base case, our symbolic executor explores the path corresponding to the recursive case. The updated path condition ∆ over X and Y is:∃n1 , n2 .X7→node( , n1 ) ∗ Y 7→node( , n2 ) ∗ pre(n1 , n2 )Executing the body of the loop, at line 5 x.next is dereferenced; hence n1 is to beaccessed. Since n1 is constrained by pre, our engine again tries two possible values forn1 resulting from LFP. For the base case, the path condition ∆ over X, Y , n1 and n2 is:∃n1 , n2 .X7→node( , n1 ) ∗ Y 7→node( , n2 ) ∧ n1 =null ∧ n2 =null

Then, n2 is accessed via y.next. Since it has been assigned to null already, there is nocase splitting. n1 =null violates the looping condition so symbolic execution finishes
exploring the path and backtracks. We obtain a test input where x and y both have one
digit. Likewise, we generate test inputs where x and y both have two digits, three digits
and so on. Note that we put a bound on the number of unfolding for loops.
In contrast to ours which always generates valid test inputs, the existing lazy approaches [36, 9, 10] would generate invalid test inputs such as (i) x and y have different
number of digits; or (ii) x and y are aliasing; or (iii) x (or y) is a cyclic linked list.

3

A Core Language

In [34], Schwartz et al. described the algorithm of symbolic execution as an extension
to the run-time semantics of a general language. The language, called SimpIL, is simple but “powerful enough to express typical languages as varied as Java and assemblycode” [34]. In this work, we use a similar presentation to describe our new symbolic
execution engine. This section introduces our core language, which is an extension of
SimpIL with operations on heap memory. Note that our implementation is for Java
bytecode, and our approach extends to other languages.
Syntax The syntax of the language is defined in Fig. 3. A program in our core language
consists of multiple data structures and statements. The primitive types include integer, boolean and void; statements consist of assignment, memory store, goto, assertion,
conditional goto, memory allocation, and memory deallocation; expressions are sideeffect free and consist of typical non-heap expressions and memory load. We use opb torepresent typical binary operators, e.g., addition, subtraction. Similarly, opu is used to[CONST][UNOP][LOAD][VAR]h, s ` k ⇓ k

k0 = opu k1

h, s ` e1 ⇓ k1

h, s ` opu e1 ⇓ k0

h, s ` v ⇓ k1

r = h(k1 )h, s ` v ⇓ s(v)[BINOP]

k2 = r(Type(v), fi )h, s ` v.fi ⇓ k2
h, s ` e ⇓ k[ASSIGN][NEW]

k0 = k1 opb k2

h, s ` e1 opb e2 ⇓ k0
l = s(v) h0 = h \ {l 7→ } ι = Σ(pc + 1)
[FREE]hΣ, h, s, pc, free vi ; hΣ, h0 , s, pc + 1, ιis0 = s[v ← k] ι = Σ[pc + 1]hΣ, h, s, pc, v := ei ; hΣ, h, s0 , pc + 1, ιih, s ` v ⇓ k1 h, s ` e ⇓ k2 r = h(k1 )r 0 =r[(Type(v), fi ) ← k2 ] h0 =h[k1 ← r 0 ] ι=Σ(pc + 1)hΣ, h, s, pc, v.fi := ei ; hΣ, h0 , s, pc + 1, ιih, s ` e ⇓ true ι = Σ(pc + 1)

ι = Σ(k)hΣ, h, s, pc, goto ei ; hΣ, h, s, k, ιi[FCOND]h, s ` null ⇓ nullh, s ` e2 ⇓ k2

hΣ, h, s, pc, v := new c(v1 , .., vn )i ; hΣ, h0 , s0 , pc + 1, ιih, s ` e ⇓ k[TCOND]h, s ` e1 ⇓ k1

fresh−map r 0 r 0 (c, fi )=s(vi ) ∀i∈{1..n} fresh l0
h0 = h[l0 ← r 0 ] s0 = s[v ← l0 ] ι = Σ(pc + 1)

[STORE][GOTO][NULL][ASSERT]hΣ, h, s, pc, assert(e)i ; hΣ, h, s, pc + 1, ιih, s ` e0 ⇓ true h, s ` e1 ⇓ k1

ι = Σ(k1 )hΣ, h, s, pc, if e0 then goto e1 else goto e2 i ; hΣ, h, s, k1 , ιih, s ` e0 ⇓ false h, s ` e2 ⇓ k2

ι = Σ(k2 )hΣ, h, s, pc, if e0 then goto e1 else goto e2 i ; hΣ, h, s, k2 , ιiFig. 2. Operational semantics of the core language
datat ::= data c { field;∗ }field ::= t v
t ::= c | ττ ::= int | bool | void
prog ::= stmt;∗
stmt ::= v := e | v.fi := e | goto e | assert e| if e0 then goto e1 else goto e2| v := new c(v1 , .., vn ) | free v
e ::= k | v | v.fi | e1 opb e2 | opu e1 | nullFig. 3. A core intermediate language

represent typical unary operators, e.g., logical negation. k represents either a 32-bit integer constant or a boolean value (true or false). The expressions used together withgoto should not contain variables. For the sake of simplicity, we assume the programs
are in the form of static single assignments and are well-typed in the standard way.
Operational semantics The concrete execution configuration of a program defined by
the syntax shown in Fig. 3 is a tuple of five components hΣ, h, s, pc, ιi. Σ is the list of
program statements; h is the current memory state (i.e., the heap); s records the current
value of program variables (i.e., the stack); pc is the program counter; and ι is thecurrent statement. Among these, Σ, h and s are mapping functions: Σ maps a number
to a statement; h maps a memory location to its content; s maps a variable to its value.
The concrete heap h of type Heaps assumes a fixed finite collection Node, a fixed
finite collection Fields, a disjoint set Loc of locations (i.e., heap addresses), a set of

non-address values Val, such that null∈Val and Val ∩ Loc = ∅. We define Heaps as:
def

Heaps = Loc*f in (Node → Fields → Val ∪ Loc)
Further, a concrete stack s is of type Stacks, defined as follows:def

Stacks = Var → Val ∪ Loc
is a mapping from a variable to a value or a memory address. We use [x ← k] to denote
updating a variable x with value k for mapping functions; for example, s[x ← 13]
denotes a new stack that is the same as stack s except that it maps variable x to thevalue 13. The operational semantics of our language is shown in Fig. 2. The rules areof the following form:
computationhcurrent statei ; hend statei
The computation in a rule is read from the top to the bottom, the left to the right, and areapplied based on syntactic pattern-matching. Given a statement, our engine finds a rule
to execute the computation on the top and returns the end state in the case of success. If
no rule matches (e.g., accessing a dangling pointer), the execution halts. In these rules,
fresh is used as an overloading function to return a new variable/address. Similarly,
fresh−map returns a new mapping and Type returns the type of a variable.
For the evaluation of expressions, we use h, s ` e ⇓ k to denote the evaluation of
expression e to a value k in the current context h and s. The application of these rules
is also based on pattern-matching similar to the application of the statements above.
For example, rule [NEW] describes the operational semantics of the command that
allocates dynamic heaps. Firstly, it creates a new mapping r0 to relate fields of the new
object to their stack values. Next, it generates a new heap entry at the fresh address l0 .
Lastly, it updates the stack value of the variable with the heap address.

4

Symbolic Execution

This section presents details on symbolic execution using a separation logic-based language to encode path conditions in heap-based programs.
Separation logic We use separation logic [20, 32] to capture symbolic heaps and expressions. Separation logic, an extension of Hoare logic, is a state-of-the-art assertion
language designed for reasoning about heap-based programs. It provides concise andprecise notations for reasoning about the heap. In particular, it supports the separating
conjunction ∗ that splits the global heap into disjoint sub-heap regions, each of which
can be analysed independently. Combined with inductive predicates, separation logic
has been shown to capture semantics of unbounded heaps, loops and recursive procedures naturally and succinctly [24, 35, 26].
In the following, we define the separation logic formulae used in this work to encode
path conditions of heap-based programs. A separation logic formula is defined by thesyntax presented in Fig. 4. We assume that c ∈ Node is a heap node; fi ∈ Fields is aΦ ::= ∆ | Φ1 ∨ Φ2
∆ ::= ∃v̄. (κ∧α∧φ)κ ::= emp | v7→c(fi :vi ) | P (v̄) | κ1 ∗κ2
α ::= true | v1 =v2 | v=null | ¬α | α1 ∧α2
φ ::= true | a1 =a2 | a1 ≤a2 | ¬φ | φ1 ∧φ2
a ::= k | v | k×a | a1 +a2 | −aPred ::= pred P1 (v̄1 )≡Φ1 ; · · · ; pred PN (v̄N )≡ΦnFig. 4. Syntax of separation logic

field; and v, vi represent variables. We notice that each kind of heap nodes c corresponds
to a data structure declared by the user using the keyword data in our core language.
We write v̄ to denote a sequence of variables. A separation logic formula is denotedas Φ, which can be either a symbolic heap ∆ or a disjunction of them. A symbolic
heap ∆ is an existentially quantified conjunction of some spatial formulae κ, somepointer (dis)equality α, and some formulae in arithmetic φ [16]. All free variables in∆, denoted by function FV(∆), are either program variables or implicitly universallyquantified at the outermost level. The spatial formula κ may be a separating conjunction(∗) of emp predicate, points-to predicates v7→c(fi :vi ), and predicate applications P (v̄).
Whenever possible, we discard fi of the points-to predicate and use its short form as
v7→c(v̄). Note that v1 6=v2 and v6=null are short forms for ¬(v1 =v2 ) and ¬(v=null)
respectively. Each inductive predicate is defined by a disjunction Φ using the keyword
pred. In each disjunct, we require that variables which are not formal parameters must
be existentially quantified. We use ∆[v1 /v2 ] for a substitution of all occurrences of v2
in ∆ to v1 .
Symbolic execution Recall that the concrete execution configuration is a 5-tuple. The
symbolic execution configuration is also a tuple of five components: hΣ, ∆, s, pc, ιiwhere ∆ is a path condition in the form of a separation logic formula defined above
and s is used to map every variable to a symbolic value7 . The rest of the components
are similar to those of the concrete execution configuration, except that symbolic valuesof variables are captured in ∆ and s. We use π (and πi ) to denote symbolic values.
Memory allocations are symbolically captured in the path condition ∆. A symbolic
execution configuration hΣ, ∆, s, pc, ιi is infeasible if ∆ is unsatisfiable. Otherwise, it
is feasible.
All operational symbolic execution rules over our language are shown in Fig. 5. In
these rules, similar to Fig. 2 we use function fresh to return a fresh variable. We illustrate the execution through rule [S−NEW]. This rule allocates a new object of typec and assigns to variable v. Firstly, it generates a fresh symbolic address l0 and updates the stack to map v to this address. Secondly, it creates new symbolic heap forl0 by separately conjoining the current path condition with a new points-to predicate
7

We use the same symbol s as in concrete setting. From the context, it should be clear as towhether we are referring to symbolic stack or concrete stack.

[S−CONST][S−UNOP][S−LOAD][S−VAR]∆, s ` k ⇓ k∆, s ` v ⇓ s(v)∆, s ` e1 ⇓ π1

[S−BINOP]∆, s ` opu e1 ⇓ opu π1∆, s ` null ⇓ null∆, s ` e1 ⇓ π1∆, s ` e2 ⇓ π2∆, s ` e1 opb e2 ⇓ π1 opb π2∃w̄.l7→c(v1 , .., vi , .., vn )∗∆, s ` v ⇓ l ∃w̄.l7→c(v1 , .., vi , .., vn )∗∆, s ` vi ⇓ πi∃w̄.l7→c(v1 , .., vi , .., vn )∗∆, s ` v.fi ⇓ πi∆, s ` v ⇓ l[S−FREE]∆, s ` e ⇓ π[S−NEW]ι = Σ(pc + 1)hΣ, ∃w̄.l7→c(...)∗∆, s, pc, free vi ; hΣ, ∃w̄.∆, s, pc + 1, ιi[S−ASSIGN]

fresh l0s0 =s[v ← π]

ι = Σ[pc + 1]hΣ, ∆, s, pc, v := ei ; hΣ, ∆, s0 , pc + 1, ιi∆0 ≡∆ ∗ l0 7→c(v1 , .., vn ) s0 =s[v ← l0 ]

ι = Σ(pc+1)hΣ, ∆, s, pc, v = new c(v1 , .., vn )i ; hΣ, ∆0 , s0 , pc+1, ιi[S−STORE]∆, s ` e ⇓ k[S−GOTO][S−NULL]l7→c(v1 , .., vi , .., vn ) ∈ ∆ ∆, s ` v ⇓ l∆, s ` e ⇓ π s0 =s[vi ← π] ι = Σ(pc + 1)hΣ, ∆, s, pc, v.fi = ei ; hΣ, ∆, s0 , pc + 1, ιi[S−ASSERT]hΣ, ∆, s, pc, goto ei ; hΣ, ∆, s, k, ιi[S−TCOND][S−FCOND]∆, s ` e0 ⇓ π0∆0 ≡∆ ∧ π∆, s ` e ⇓ π

ι = Σ(k)∆, s ` e1 ⇓ k1

ι = Σ(pc+1)hΣ, ∆, s, pc, assert(e)i ; hΣ, ∆0 , s, pc+1, ιi∆0 ≡∆∧π0ι = Σ(k1 )hΣ, ∆, s, pc, if e0 then goto e1 else goto e2 i ; hΣ, ∆0 , s, k1 , ιi∆, s ` e0 ⇓ π0∆, s ` e2 ⇓ k2

∆0 ≡∆∧¬π0ι = Σ(k2 )hΣ, ∆, s, pc, if e0 then goto e1 else goto e2 i ; hΣ, ∆0 , s, k2 , ιiFig. 5. Symbolic operational execution rules

l0 7→c(v1 , .., vn ). Lastly, it loads the next statement using the program counter. Note that
we assume each variable vi is only used to create at most one new object.
Rule [S−FREE] symbolically de-allocates the heaps. To capture the de-allocatedheaps for test input generation, we keep track the corresponding points-to predicatesby storing them in a “garbage” formula. At the end of execution, those predicates areplugged into the current path condition before being used to generate test inputs.

5

Lazy Test Input Generation

In this section, we present the test input generation based on the symbolic execution
engine we depicted in the previous sections. The inputs of our method are a programprog in the language we defined in Section 3 and an optional precondition ∆pre in theform of a separation logic formula defined in Section 4. The output is a set of fully
initialized test inputs that satisfy the precondition and often achieve high test coverage.
Our method is based on lazy initialization. The main difference between our method andprevious approaches based on lazy initialization is that we generate values of reference
variables and fields in a context-sensitive manner.
Our symbolic execution engine starts with the configuration: hΣ, ∆pre σ, s0 , pc0 , ι0 i
where σ is a substitution of input variables to their corresponding symbolic values, s0 is
an initial mapping of input variables to symbolic values, pc0 and ι0 denote the first valueof the program counter and the first statement respectively. The engine systematically

Algorithm 1: Procedure LFP
SVi ←{Pi (t̄i )} ; Ai ←false ;/* i ∈ {1..N} */while true do
3
SVi0 ←{} ;/* i ∈ {1..N} */4foreach i ∈ {1..N } do
5foreach ∆j ∈ SVi do
6
SVi0 ←SVi0 ∪ unfold(∆j ) ;W
7
A0i ← {∃w̄.abs(Π(κ∧α, t̄i ), t̄i ) | (∃w̄.κ∧α∧φ) ∈ SVi0 } ;

1

2

8
9
10
11

if ∀i ∈ {1..N }. A0i ⇒ Ai then¯ ;return SV
else
SVi ←SVi0 ; Ai ←A0i ;/* fixed point *//* i ∈ {1..N} */derives the strongest postcondition of every program path (with a bound on the numberof loop unfolding), by applying the symbolic operational execution rules (i.e., shown in
Fig. 5). After obtaining the strongest post-state, our engine invokes S2SATSL to check
whether or not the resultant symbolic heap is satisfiable, and generate a model if it is.
The model is then transformed into a test input.
Context-sensitive lazy initialization Recall that lazy initialization [21] leaves a reference variable or field uninitialized until it is first accessed and then enumerates all
possible valuations of the variable or field. For instance, as shown in Figure 5, a reference variable or field can be accessed in the rules [S−VAR], [S−LOAD], [S−STORE],or [S−FREE]. The problem is that many valuations obtained through enumeration are invalid (i.e., violating the precondition). Thus, in this work, we propose context-sensitive
enumeration. When an uninitialized reference variable or field with symbolic value
v is accessed during symbolic execution, procedure enum(v, ∆, s) is invoked to nondeterministically initialize v with values derived from the symbolic execution context,
i.e., ∆ and s. For each value of the set, the symbolic execution engine creates a new
branch for exploration. Procedure enum(v, ∆, s) works based on the following three
scenarios.
1. If ∆, s implies that v has previously been initialized to either null (i.e., v = null)or a points-to predicate (i.e., v7→ ∈ ∆), initializing again is not necessary.
2. If v is uninitialized and there does not exist a predicate Pi (v̄i ) in ∆ such that v ∈ v̄i(i.e., v is not constrained by the context), v is initialized to null, to a new points-to
predicate with uninitialized fields, or to a points-to predicate in ∆.
3. If v is uninitialized and there exists some predicate Pi (v̄i ) in ∆ such that v ∈ v̄i(i.e., v is constrained by the predicate), we substitute Pi by SVi to get a set of
possible values of v which are consistent with the context ∆. SVi is computed
using the least fixed point analysis as shown below.
Least fixed point analysis We assume that there are N predicate definitions P1 (t̄1 ), ...,¯ for
PN (t̄N ) (P for short). We then use the procedure LFP to compute SV1 , ..., SVN (SVshort) according to each predicate. Each SVi stores all possible contexts (in the form of¯ ,separation logic formulae) for t̄i that could be derived from Pi (t̄i ). After having all SV
in scenario 3 mentioned above, we substitute Pi (v̄i ) with SVi [v̄i /t̄i ] to get all possible
values for v. Because of the substitution, new variables may be introduced in ∆, we
update s accordingly by using the variables’ names as their symbolic values. Note that¯ once before running the symbolic execution engine.
we only compute SV
The details of LFP are shown in Algorithm 1. LFP takes the set of predicate defi¯ of all predicates.
nitions P as input. It outputs the set of symbolic heap formulae SV
In this algorithm, each Ai , a disjunctive base formula (i.e., a formula without any occurrence of inductive predicates), captures the abstraction of all formulae in accordancewith SVi . In intuition, LFP iteratively explores each SVi (initialized with {Pi (t̄i )} atline 1) into a set of disjoint, complete and “smaller” contexts. At the same time, it computes an abstraction Ai over heap allocations and (dis)equality constraints over t̄i . If
the fixed point (at lines 8-9) is achieved, LFP stops. Otherwise, it moves to the next
iteration.
In particular, for the first task LFP enumerates all possible symbolic heap locations which t̄i can be assigned to. The enumeration is performed through the function
unfold(∆j ) (at line 6), which replaces every occurrence of inductive predicates in ∆jby their corresponding definitions with α-renaming. As a result, each disjunct in SVi
generates a new context.
For the second task, after the new contexts have been derived, at line 7, LFP computes an abstraction on the set of symbolic values which every parameter t̄i can be
assigned to. This abstraction is critical for the termination of the algorithm and is computed with two functions. Intuitively, these two functions compute constraints on parameters of each inductive predicate. The first function abs(κ ∧ α, t̄i ) captures thereference values of t̄i , while the second function Π(κ ∧ α, t̄i ) captures (dis)equality
constraints on t̄i .
In particular, the function abs is defined as abs(emp ∧ α, v̄) = emp ∧ α. Otherwise,(
v7→c(w̄) ∗ abs(κ1 ∧ α, v̄) if v∈v̄abs(v7→c(w̄) ∗ κ1 ∧ α, v̄) =abs(κ1 ∧ α, v̄)otherwise(
false
if w̄ ∩ v̄ 6= ∅abs(P (w̄) ∗ κ1 ∧ α, v̄) =abs(κ1 ∧ α, v̄) otherwise

In principle, this function retains all heap nodes allocated by variables in v̄, maps
inductive predicates with arguments in v̄ to false, and discards other constraints in κ.
The function Π(κ∧α, v̄) eliminates (dis)equality constraints in κ∧α on all variables
which are not in v̄. In particular, Π(κ ∧ true, v̄)=κ ∧ true, Π(κ ∧ false, v̄)=false,and Π(κ ∧ v1 6=v1 ∧ α1 , v̄)=false. Otherwise,Π(κ ∧ α1 [null/v1 ], v̄)Π((κ ∧ α )[v /v ], v̄)121
Π(κ ∧ v1 =e ∧ α1 , v̄) =

Π((κ
∧
α
)[v
/v
1
1
2 ], v̄)( Π(κ ∧ α1 , v̄) ∧ v1 =eΠ(κ ∧ v1 6=e ∧ α1 , v̄) =Π(κ ∧ α1 , v̄) ∧ v1 6=eΠ(κ ∧ α1 , v̄)if e=null ∧ v1 6∈v̄if e=v2 ∧ v1 6∈v̄if e=v2 ∧ v2 6∈v̄ ∧ v1 ∈v̄
otherwise
if e=null ∧ v1 ∈v̄ ∨ e=v2 ∧ v1 ∈v̄ ∧ v2 ∈v̄
otherwiseAn equality v1 =v2 is retained if both v1 and v2 are in v̄. Otherwise, it is eliminatedand one of the variables must be eliminated via a substitution. A disequality v1 6=v2 isretained if both v1 and v2 are in v̄. Otherwise, it is eliminated. Similarly, v1 =null andv1 6=null are retained if v1 is in v̄. After applying the above two functions, formulae
may contain redundant variables in ∃w̄, which may be eliminated.
Correctness Correctness of the proposed enumeration method follows the correctnessof the procedure LFP. We argue that LFP is sound (i.e., all generated values are correct),terminating, and complete (i.e., all possible heap and (dis)equality constraints between
reference parameters in each predicate are captured at fixed point).
Theorem 1 (Soundness). If ∆j ∈ SVi and h, s |= ∆j then h, s |= Pi (t̄i ).
Proof. The soundness of LFP follows the correctness
W of the unfolding, i.e., ∆j is derived through the unfolding of Pi (t̄i ) and Pi (t̄i ) ≡ {∆j | ∆j ∈ SVi }. Hence, ∆j isan under-approximated formula of Pi (t̄i ).
Theorem 2 (Termination). Suppose M be the maximal arity among the inductive
2
predicates Pi (t̄i ), i ∈ {1..N }. Then LFP runs in O(N 2M +M ).
Proof. The complexity of LFP relies on the number of disjuncts computed by two functions abs(κ∧α, t̄i ) and Π(κ∧α, t̄i ). It comes from the following three sub-components.
• As the maximal arity of t̄i is M , the number of (dis)equalities among these variables2
is O(M 2 ). The number of its subsets is O(2M ).
• Furthermore, the maximum number of points-to predicates is M . Hence, the number of its subsets is O(2M ).
• There are N predicate definitions in the system.
Hence, the implication at line 8 in Algorithm 1 holds in a finite number of iterations.
Theorem 3 (Completeness). If h, s |= Pi (t̄i ) then ∃∆j ∈ SVi s.t. h, s |= ∆j . Moreover, SVi captures all possible heap and (dis)equality constraints between reference
variables in t̄i .
Proof. The first part follows the correctness of the unfolding. For the second part, noticethat at least one of A1 , ..., AN gets weaker via each iteration until all of them reach
fixed point. Each Ai is derived from its according SVi by two functions abs(κ∧α, t̄i )and Π(κ ∧ α, t̄i ), which captures all heap and (dis)equality constraints between t̄i .
Example 1. We demonstrate the computation of SV for predicate pre(a, b) in Section
2. The computation is summarized in Fig. 6 where i is the number of the iteration.
Since A2 ⇒ A1 , LFP stops after two iterations and produces SV 1 as the set of newcontexts for this example. After that, the engine substitutes SV 1 into ∆ to obtain thetwo corresponding symbolic heaps.

i
0
1

2

SV i
pre(a, b)
emp ∧ a=null ∧ b=null∨∃n1 , n2 .a7→node( , n1 )∗b7→node( , n2 )∗pre(n1 ,n2 )emp ∧ a=null ∧ b=null∨∃n1 , n2 .a7→node( , n1 )∗b7→node( , n2 ) ∧ n1 =null ∧ n2 =null∨∃n1 , n2 , n3 , n4 .a7→node( , n1 )∗b7→node( , n2 )∗n1 7→node( , n3 )∗n2 7→node( , n4 )∗pre(n3 ,n4 )

Ai
false
emp ∧ a=null ∧ b=null∨ ∃n1 , n2 .a7→node( , n1 )∗b7→node( , n2 )emp ∧ a=null ∧ b=null∨ ∃n1 , n2 .a7→node( , n1 )∗b7→node( , n2 )∨ ∃n1 , n2 .a7→node( , n1 )∗b7→node( , n2 )Fig. 6. LFP for the motivating example
Table 1. Experimental results
JSF
JBSE
BBE
#Tests Cov.(%) #Calls T(s) #Tests Cov.(%) NCov.(%) T(s) #Tests Cov.(%) NCov.(%) T(s)
DLL
74/74
100
325 49 121/5146
56100
206 0/35
0
21
21
AVL
69/69
100
623 400 76/295
100
100
48 17/117
70
89
69
RBT
314/314 100
2070 2256 137/291
87
91
38 14/380
26
53
333
SUSHI
7/7
100
30
5
0/900
0
100
24 2/27
25
25
8
TSAFE
5/5
24
13
3
0/32
0
5
10
0/1
0
0
1
Gantt
21/21
100
140 25 17/887
55
90
24
0/6
0
5
2
SLL
26/26
100
55
11
- 16/50
66
71
19
Stack
18/18
100
31
7
- 11/1484
84
6
BST
182/182 100
698 241- 19/260
69
86
131
AAT
103/103 100
1179 1981- 3/166
6
43
111
Tll
3/3
100
11
2
1/4
38
50
2
Program6

Implementation and Evaluation

We have implemented our approach described in previous sections into a tool, called
Java StarFinder (JSF), consisting of 11569 lines of Java code. The architecture of JSF
was briefly described in our previous work [30]. In the following, we evaluate JSF inorder to answer three research questions (RQ). All experiments are conducted on alaptop with 2.20GHz Intel Core i7 and 16 GB RAM.
Our experimental subjects include Singly Linked List (SLL), Doubly Linked List
(DLL), Stack, Binary Search Tree (BST), and Red Black Tree (RBT) from SIR [4];AVL Tree (AVL) and AA Tree (AAT) from Sierum/Kiasan [5], the motivation example, TSAFE project, and Gantt project used in SUSHI [8] and a data structure called Tll[23]. Since JSF is yet to support string, array, and object oriented features such as inheritance and polymorphism, we exclude data structures and methods which rely on thesefeatures, i.e., Disjoint Set in Sierum/Kiasan and Google Closure in SUSHI. Supportingthese features is left for future work. In total, our experiment subjects include a total of
74 methods, whose lines of code range from dozens to more than one thousand.
RQ1: Can JSF reduce invalid test inputs? To answer this question, we need to check
whether a generated test input is valid or not. In the benchmark programs which wecollect, six data structures contain repOK methods which are designed to check if the
input is valid or not, i.e., Stack, DLL, BST, RBT, AVL, and AAT. In addition, the motivation example in SUSHI is based on DLL and thus we use the method repOK of DLL tovalidate its test inputs. We write the repOK methods manually for the remaining test
subjects. For SLL and Tll, we write their repOK methods based on their standard def-

inition. For TSAFE and Gantt, we write their repOK methods after reading the source
code, i.e., the repOK encodes the condition required to avoid RuntimeException
such as N ullP ointerException.
For each generated test input, we check its validity by passing it as arguments to thecorresponding repOK method [36]. If repOK returns true, the test input is deemedvalid. As a baseline, we compare JSF with JBSE [10], which implements the HEX approach [9], and the black box enumeration (BBE) approach documented in [36]. We do
not compare with the white box enumeration approach [36] as it requires user-provided
conservative repOK methods, which are missing in these benchmarks. Note that conservative repOK methods are different from repOK methods, and writing those methods is highly nontrivial. We do not compare our approach with SUSHI because SUSHI
generates test cases in form of sequence of method calls whereas we generate test cases
in form of input data structures. SUSHI and our approach are thus complementary toeach other. To run JBSE, we need invariants written in HEX. We manage to find invariants for DLL, RBT, AVL, TSAFE, and Gantt from [6], and thus we are able to run
JBSE on these subjects. It is not clear to us how to write HEX invariants for other data
structures or if HEX is expressive enough to describe them.
The experimental results are shown in Table 1, where the first column show thename of test subjects, and the last three columns show the results of JSF, JBSE, andBBE respectively. Columns #Tests show the results in form of the number of valid test
inputs over the number of generated test inputs. Note that because JBSE generate partial
initialized test inputs, we add an additional call to repOK method after the method
under test to concretize their test inputs. The results show that, as expected, every test
input generated by JSF is valid. In comparison, JBSE generates 4.65% valid test inputs
and BBE generates 7.83% valid test inputs. From the results, we conclude that JSF iseffective in generating valid test inputs.
RQ2: Can JSF generate test inputs that achieve high code coverage? To answer thisquestion, we use JaCoCo [2] to measure the branch coverage of test inputs generated
by the tools. The results are shown in the columns titled Cov.(%) and NCov.(%) in
Table 1. The columns NCov.(%) show the coverage of all generated test inputs, thecolumns Cov.(%) show the coverage of test inputs that satisfy repOK methods. As all
test inputs generated by JSF satisfy repOK methods, the result of JSF has only one
column Cov.(%).
For 73/74 methods (including auxiliary methods), JSF can achieve 100% branchcoverage (excluding infeasible branches). The only exception is method T S R 3 in the
TSAFE project. It is because this method invokes native methods and handling native
methods is beyond the capability of JSF at the moment. In general, JSF achieves 98.98%
coverage on average. In comparison, when considering all test inputs, JBSE achieves
95.59% coverage on average and BBE achieves 54.66% coverage on average. Sincemany of these test inputs are invalid, these coverage are inflated. When considering only
test inputs that satisfy repOK method, JBSE is only able to achieve 68.54% coverageon average and BBE achieves 37.85% coverage on average. From these results, weconclude that JSF can generate test inputs with high branch coverage for the methods
under test.

RQ3: Is JSF sufficiently efficient? To answer this question, we measure the time spent togenerate test inputs for each method. The results are shown in the columns titled T(s) in
Table 1. From the results, JBSE and BBE are clearly faster than JSF. That is, JBSE andBBE takes average 8.75 and 9.50 seconds respectively to handle each method, whereas
JSF’s time ranges from 1 second to half an hour, with an average of 67.29 seconds per
method. We also report the number of solver calls used by JSF. In average, JSF needs
70 calls per method. The main reason JSF is slower than JBSE and BBE is JSF has tosolve harder path conditions with inductive predicates. However, the efficiency of JBSE
and BBE comes with the tradeoff of excessive number of invalid test inputs as discussed
above, whereas JSF only generates valid test inputs. From these results, we conclude
that JSF is slower than JBSE and BBE, but still sufficiently efficient to provide higher
quality results.

7

Related Work

This work is based on generalized symbolic execution (GSE) [21], which is the stateof-the-art way for the symbolic execution [22] of heap-based programs. At the heart of
GSE is the lazy initialization algorithm which executes programs on inputs with reference variables and fields being uninitialized. When a reference variable or field is first
accessed, lazy initialization enumerates all possible heap objects that it can: (i) be null,(ii) point to a new object with all reference fields being uninitialized, or (iii) point to any
previously initialized object of the same type. This explicit enumeration quickly leads
to path explosion in any non-trivial program, and existing approaches to addressing thisproblem can be roughly grouped into two categories:• State merging approaches group together the choices of lazy initialization. For instance, the work in [14, 15] represented the choices (ii) and (iii) with a variable,
while the work in [19] captured all choices (i), (ii) and (iii) in a symbolic heap using guarded value set. Those work cannot avoid path explosion, but delay it to laterstage [14, 15], or delegate the burden to an SMT solver [19].
• State prunning approaches [36, 33, 9] truly mitigate the path explosion problem
by using a precondition to describe some properties of the input. After explicitly
enumerating all possible choices, i.e. both valid and invalid paths, these approaches
will prune the invalid paths that violate the precondition.
A principle difference between our work and the aforementioned approaches is that
we use separation logic, which is expressive enough to define abitrary unbounded data
structures. Consequently, we are able to construct valid choices from the definition,
without explicit enumeration of invalid paths, and without false positives. We discuss
some notable state prunning approaches in the following.
repOK As GSE with lazy initialization results in partially initialized structures containing both concrete and symbolic values, the work in [36] propose to use a particularkind of repOK, called conservative or hybrid repOK, that returns true when running
into parts of the structure that are still symbolic. This, of course, leads to false positives.

JML The BLISS approach in [33] used both hybrid repOK and JML [27] together as
preconditions. The JML precondition is used to precompute relational bounds on theinterpretation of class fields. It is translated into a SAT problem by the TACO tool [17].
As pointed out in [18], this translation introduces duplication, which undermines thebenefit of eliminating invalid structures when the size is big. BLISS uses symmetry
breaking and refine bounds to mitigate this problem.
HEX Braione et al. [9] introduced Heap EXploration Logic (HEX) as a specification
language to constrain heap inputs. However, the language is not expressive enough todescribe many common data structures, and users have to provide additional methods,
called triggers [3], to check the properties that cannot be written in HEX. Moreover,HEX does not support numerical constraints, and it represents unbounded data structures using regular operators (using (π)+ operator). Therefore, it is unable to capture
the non-regular data structures, e.g., singly-linked lists which have 2n nodes (n≥0) andthe content of each node is 0. Finally, it is unclear how the HEX solver discharges anunbounded heap formula with regular operators.
Separation logic Our work is also related to research on Smallfoot symbolic execution [7] and its following work, e.g. [13, 29]. Those work are not based on lazy initialization, and it is not clear how they can be used for test input generation. Our work is
the first to explore the use of separation logic for testing.

8

Conclusion and Future Work

We present a symbolic execution framework for heap-based programs using separation logic. Our novelty is the proposed context-sensitive lazy initialization for test input
generation. The experimental results show that our approach significantly reduces thenumber of invalid test inputs and improves the test coverage. For future work, we plan
to integrate our approach on a dynamic symbolic execution engine (e.g., JDart [28]).
We might combine JSF with bi-abduction and frame inference tools (i.e., Infer [1, 12],
S2 [23, 25]) to both verify safety and generate test inputs to locate/confirm real bugs
in heap-based programs. Finally, we are actively investigating the use of JSF tool for
automatic program repair, a preliminary results were reported in [37].
Acknowledgments. This research is supported by MOE research grant MOE2016-T22-123.

References
1. Facebook Infer. http://fbinfer.com/
2. JaCoCo. http://www.eclemma.org/jacoco/
3. JBSE. https://github.com/pietrobraione/jbse
4. SIR. http://sir.unl.edu/portal/index.php
5. Sireum. https://code.google.com/archive/p/sireum/downloads

6. SUSHI Experiments.
https://github.com/pietrobraione/sushi-experiments
7. Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi,
K. (ed.) APLAS 2005, pp. 52–68. Springer (2005). https://doi.org/10.1007/11575467 5
8. Braione, P., Denaro, G., Mattavelli, A., Pezzè, M.: Combining Symbolic Execution and
Search-based Testing for Programs with Complex Heap Inputs. In: Bultan, T., Sen, K. (eds.)
ISSTA 2017, pp. 90–101. ACM (2017). https://doi.org/10.1145/3092703.3092715
9. Braione, P., Denaro, G., Pezzè, M.: Symbolic Execution of Programs with Heap Inputs.
In: Nitto, E.D., Harman, M., Heymans, P. (eds.) FSE 2015, pp. 602–613. ACM (2015).
https://doi.org/10.1145/2786805.2786842
10. Braione, P., Denaro, G., Pezzè, M.: JBSE: A Symbolic Executor for Java Programs with
Complex Heap Inputs. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) FSE 2016, pp.
1018–1022. ACM (2016). https://doi.org/10.1145/2950290.2983940
11. Cadar, C., Godefroid, P., Khurshid, S., Păsăreanu, C.S., Sen, K., Tillmann, N., Visser, W.:
Symbolic Execution for Software Testing in Practice: Preliminary Assessment. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) ICSE 2011, pp. 1066–1071. ACM (2011).
https://doi.org/10.1145/1985793.1985995
12. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional ShapeAnalysis by Means of Bi-Abduction. JACM 58(6), 26:1–26:66 (2011).
https://doi.org/10.1145/2049697.2049700
13. Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated Verification of Shape, Size and
Bag Properties via User-defined Predicates in Separation Logic. Sci. Comput. Program.
77(9), 1006–1036 (2012). https://doi.org/10.1016/j.scico.2010.07.004
14. Deng, X., Lee, J., Robby: Bogor/Kiasan: A K-bounded Symbolic Execution for Checking
Strong Heap Properties of Open Systems. In: ASE 2006, pp. 157–166. IEEE Computer Society (2006). https://doi.org/10.1109/ASE.2006.26
15. Deng, X., Robby, Hatcliff, J.: Towards A Case-Optimal Symbolic Execution Algorithm for
Analyzing Strong Properties of Object-Oriented Programs. In: SEFM 2007. IEEE Computer
Society (2007). https://doi.org/10.1109/SEFM.2007.43
16. Enderton, H.B.: A Mathematical Introduction to Logic (Second Edition), pp. 67–181. Academic Press (2001). https://doi.org/10.1016/B978-0-08-049646-7.50008-4
17. Galeotti, J.P., Rosner, N., López Pombo, C.G., Frias, M.F.: Analysis of Invariants for Efficient
Bounded Verification. In: Tonella, P., Orso, A. (eds.) ISSTA 2010, pp. 25–36. ACM (2010).
https://doi.org/10.1145/1831708.1831712
18. Geldenhuys, J., Aguirre, N., Frias, M.F., Visser, W.: Bounded Lazy Initialization. In:
Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013, pp. 229–243. Springer (2013).
https://doi.org/10.1007/978-3-642-38088-4 16
19. Hillery, B., Mercer, E., Rungta, N., Person, S.: Exact Heap Summaries for Symbolic Execution. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016, pp. 206–225. Springer (2016).
https://doi.org/10.1007/978-3-662-49122-5 10
20. Ishtiaq, S.S., O’Hearn, P.W.: BI as an Assertion Language for Mutable Data Structures. In: Hankin, C., Schmidt, D. (eds.) POPL 2001, pp. 14–26. ACM (2001).
https://doi.org/10.1145/360204.375719
21. Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized Symbolic Execution for Model
Checking and Testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003, pp. 553–568. Springer(2003). https://doi.org/10.1007/3-540-36577-X 40
22. King, J.C.: Symbolic Execution and Program Testing. Commun. ACM 19(7), 385–394(1976). https://doi.org/10.1145/360248.360252
23. Le, Q.L., Gherghina, C., Qin, S., Chin, W.N.: Shape Analysis via Second-Order BiAbduction. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 52–68. Springer (2014).
https://doi.org/10.1007/978-3-319-08867-9 4

24. Le, Q.L., Sun, J., Chin, W.N.: Satisfiability Modulo Heap-Based Programs. In: Chaudhuri,S., Farzan, A. (eds.) CAV 2016, pp. 382–404. Springer (2016). https://doi.org/10.1007/9783-319-41528-4 21
25. Le, Q.L., Sun, J., Qin, S.: Frame Inference for Inductive Entailment Proofs in Separation Logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, pp. 41–60. Springer (2018).
https://doi.org/10.1007/978-3-319-89960-2 3
26. Le, Q.L., Tatsuta, M., Sun, J., Chin, W.: A Decidable Fragment in Separation Logic with
Inductive Predicates and Arithmetic. In: Majumdar, R., Kuncak, V. (eds.) CAV 2017, pp.
495–517. Springer (2017). https://doi.org/10.1007/978-3-319-63390-9 26
27. Leavens, G.T., Baker, A.L., Ruby, C.: JML: A Notation for Detailed Design. In: Kilov, H.,
Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp.
175–188. Springer (1999). https://doi.org/10.1007/978-1-4615-5229-1 12
28. Luckow, K., Dimjašević, M., Giannakopoulou, D., Howar, F., Isberner, M., Kahsai, T., Rakamarić, Z., Raman, V.: JDart: A Dynamic Symbolic Analysis Framework. In: Chechik, M.,
Raskin, J.F. (eds.) TACAS 2016, pp. 442–459. Springer (2016). https://doi.org/10.1007/9783-662-49674-9 26
29. Müller, P., Schwerhoff, M., Summers, A.J.: Automatic Verification of Iterated Separating
Conjunctions using Symbolic Execution. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, pp.
405–425. Springer (2016). https://doi.org/10.1007/978-3-319-41528-4 22
30. Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J., Qin, S.: Testing Heap-based Programs with Java
StarFinder. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) ICSE 2018, pp.
268–269. ACM (2018). https://doi.org/10.1145/3183440.3194964
31. Păsăreanu, C.S., Visser, W., Bushnell, D., Geldenhuys, J., Mehlitz, P., Rungta, N.: Symbolic
PathFinder: Integrating Symbolic Execution with Model Checking for Java Bytecode Analysis. Autom. Softw. Eng. 20(3), 391–425 (2013). https://doi.org/10.1007/s10515-013-0122-2
32. Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002,
pp. 55–74. IEEE Computer Society (2002). https://doi.org/10.1109/LICS.2002.1029817
33. Rosner, N., Geldenhuys, J., Aguirre, N., Visser, W., Frias, M.F.: BLISS: Improved Symbolic
Execution by Bounded Lazy Initialization with SAT Support. IEEE Trans. Software Eng.
41(7), 639–660 (2015). https://doi.org/10.1109/TSE.2015.2389225
34. Schwartz, E.J., Avgerinos, T., Brumley, D.: All You Ever Wanted to Know about Dynamic
Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask). In:
S&P 2010, pp. 317–331. IEEE Computer Society (2010). https://doi.org/10.1109/SP.2010.26
35. 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, pp. 423–443.
Springer (2016). https://doi.org/10.1007/978-3-319-47958-3 22
36. Visser, W., Pǎsǎreanu, C.S., Khurshid, S.: Test Input Generation with Java PathFinder.
In: Avrunin, G.S., Rothermel, G. (eds.) ISSTA 2004, pp. 97–107. ACM (2004).
https://doi.org/10.1145/1007512.1007526
37. Zheng, G., Le, Q.L., Nguyen, T., Phan, Q.S.: Automatic Data Structure Repair using Separation Logic. In: JPF 2018