Interacting via the Heap in the Presence of Recursion
Jurriaan Rot

Irina Măriuca Asăvoae

Frank de Boer

LIACS, Leiden University
The Netherlands
jrot@liacs.nl

Faculty of Computer Science
Alexandru Ioan Cuza University
Romania
mariuca.asavoae@info.uaic.ro

Centrum Wiskunde en Informatica (CWI)
The Netherlands
LIACS, Leiden University
The Netherlands
frb@cwi.nl

Marcello M. Bonsangue

Dorel Lucanu

LIACS, Leiden University
The Netherlands
marcello@liacs.nl

Faculty of Computer Science
Alexandru Ioan Cuza University
Romania
dlucanu@info.uaic.ro

Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields.
In the presence of recursive procedures and local variables the interactions of a program with the
heap can become rather complex, as an unbounded number of objects can be allocated either on the
call stack using local variables, or, anonymously, on the heap using reference fields. As such a static
analysis is, in general, undecidable.
In this paper we study the verification of recursive programs with unbounded allocation of objects, in a simple imperative language for heap manipulation. We present an improved semantics for
this language, using an abstraction that is precise. For any program with a bounded visible heap,
meaning that the number of objects reachable from variables at any point of execution is bounded,
this abstraction is a finitary representation of its behaviour, even though an unbounded number of
objects can appear in the state. As a consequence, for such programs model checking is decidable.
Finally we introduce a specification language for temporal properties of the heap, and discuss model
checking these properties against heap-manipulating programs.

1

Introduction

One of the major problems in model checking recursive programs which manipulate dynamic linked
structures is that the state space is infinite, since programs may allocate an unbounded number of objects
during execution by updating reference fields (pointers). Indeed model checking and reachability for
such programs are undecidable, in general. Consequently to allow a restricted form of model checking
we need to impose either some syntactic restrictions on the program [7] or some suitable bounds on its
model. A natural bound for model checking programs without necessarily restricting their capability of
allocating an unbounded number of objects is to impose constraints on the size of the visible heap [4].
The visible heap consists of those objects which are reachable from the variables in the scope of the
currently executed procedure. Such a bound still allows for storage of an unbounded number of objects
onto the call-stack, using local variables.
In this paper we introduce a method for model checking sequential imperative programs with pointers
and recursive procedure calls. In order to allow implementation of model checking of unbounded object
allocation in the context of a bounded visible heap, we introduce a new mechanism for the generation
of fresh object identities which allows for the reuse of object identities and which includes a renaming
c J. Rot, I.M. Asăvoae, F.S. de Boer, M.M. Bonsangue, D. Lucanu
M. Carbone, I. Lanese, A. Silva, A. Sokolova (Eds.):
5th Interaction and Concurrency Experience (ICE’12). This work is licensed under the
EPTCS 104, 2012, pp. 99–113, doi:10.4204/EPTCS.104.9Creative Commons Attribution License.

100

Interacting via the Heap in the Presence of Recursion

scheme to resolve possible resulting name clashes. We introduce a formal operational semantics based
on this mechanism for an abstract programming language, called Shylock. Subsequently we introduce
a logic for reasoning about properties of the heap, where we use atomic propositions defined as regular
expressions in what is basically a Kleene algebra with tests [13]. Namely, the global and local variables
of a program are used as nominals, whereas the pointers (reference fields) constitute the set of basic
actions.
Our renaming mechanism allows a different kind of reuse of object identities than usual garbage
collection techniques. A garbage collector typically reuses object identities from the heap and considers
objects on the call stack as still in use. In contrast our technique is more tailored towards model checking,
and as such, we need to reuse as much object identities as possible to guarantee a representation of program behaviour in terms of a finite pushdown system with a finite stack alphabet. In fact, our mechanism
allows to reuse objects allocated in the call stack, that may become active when procedures return.
Structure of the paper In the next paragraph we briefly discuss related work. We introduce Shylock
and its formal semantics in Section 2. In Section 3 the abstraction of this semantics is introduced, together
with a proof of its correctness. Then in Section 4 we define a logic for temporal properties of heaps, and
finally in Section 5 we conclude.
Related work We introduce a novel technique for resolving name clashes in the context of reuse of
object identities. It is based on the concept of cut points as introduced in [19] to support static analysis
via abstract interpretation techniques. Cut points are objects in the heap that are referred to from both
local and global variables, and as such are subject to modifications during a procedure call. Recording
cut points in extra logical variables allows for a precise abstract execution of the program, which in case
of a bound on the visible heap can be represented by a finitary structure, namely that of a finite pushdown
system.
In [4] a language is studied with the same features as our Shylock programs extended with a bounded
form of concurrency. Because concurrency is an orthogonal dimension to the vertical growing of the
number of objects due to recursion and the horizontal growing due to the anonymous field update, we
have decided not to incorporate it in our Shylock language. In fact, bounded concurrency could easily be
handled with a technique similar to the one used in [4]. The novelty of our work is not in the decidability
result, which is indeed similar to that obtained in [4], but in the technique we used to obtain it. While [4]
uses finite graphs and graph isomorphisms to represent heaps and avoid name clashes, respectively, our
approach is purely symbolic, and, therefore, directly usable for model checking temporal properties of
heaps. We discuss the relationship with [4] in more detail in the final paragraph of Section 4.
Currently there are several model checkers for object oriented languages. Java Path Finder [12] is
basically a Java Virtual Machine that executes a Java program not just once but in all possible ways,
using backtracking and restoring the state during the state-space exploration. Even if Java Path Finder is
capable of checking every Java program, the number of states stored during the exploration is a limit on
what can be effectively checked. As with JCAT [8], Java source code can be translated into Promela, the
input language of SPIN. Since Promela does not support dynamic data structures, fixed-size heaps and
stacks have to be allocated.
Bandera [6] is an integrated collection of tools for model checking concurrent Java software using
state-of-the art abstraction, partial order reductions and slicing techniques to reduce the state space. It
compiles Java source code into a reduced program model expressed in the input language of other existing
verification tools. For example, it can be combined with the SAL (Symbolic Analysis Laboratory) model

J. Rot, I.M. Asăvoae, F.S. de Boer, M.M. Bonsangue, D. Lucanu

101

checker [17] that uses unbounded arrays whose sizes vary dynamically to store objects. In order to
explore all reachable states model checking is restricted to Java programs with a bounded (but not fixed
a priori) number of created objects.
TOPICS [14, 11] is a tool which aims to find certain types of bugs in non-recursive C programs
which manipulate a restricted type of heaps containing only single-linked lists. The faults detected by
TOPICS are of several types, namely: memory leak, segmentation faults, array out of bounds errors,
and usage of undefined objects in tests. The method used for bug-detection is based on reachability
analysis on counter machines. The transformation of a C program into a counter machine goes through
the intermediate representation of pointer machines which abstracts away the contents of the cells of the
linked lists.
The problem of reusing object identities has already been faced when defining semantic models
for the pi-calculus, most notably in history-dependent automata [16], a model based on the theory of
named sets capable of finite-state verification of processes that can allocate fresh resources [5]. Model
checking of a possibly unbounded number of objects with pointers but for a language with a restricted
form of recursion (tail recursion) and no block structure has been studied using high level allocation
Büchi automata [9] that allow for a finite state symbolic semantics very similar to ours. Full recursion,
but with a fixed-size number of objects is instead considered in jMoped [10], using a pushdown structure
to generate an infinite state system.
The techniques described in this paper aim at verifying programs by model checking. This is fundamentally different from other tools and techniques for verifying programs manipulating the heap by
deductive verification methods, such as separation logic [18]. Automated methods for proving annotated
programs is a very active area of research (see e.g. [15, 2, 3]). For a more detailed discussion we refer
to [3].
Acknowledgments We would like to thank the anonymous referees for their extensive comments and
suggestions that greatly improved the presentation of our work. The research of Jurriaan Rot has been
supported by the Dutch NWO project CoRE.

2

Shylock: a language to manipulate the heap

In this section we introduce Shylock, a simple imperative programming language that allows us to focus
on dynamic pointer structures in the context of recursive procedures with local variables. Programs
consist of a set of recursive procedures that can create new objects, and store them into their local or
global variables. Besides being dynamically allocated, objects can be referenced by other objects via
object fields, and exist as long as they are reachable in the heap from some other object or from a
variable. To simplify the presentation objects are the only data structure of Shylock.
We assume an infinite set V of variables ranged over by x, y, including a finite collection G of global
program variables {g1 , g2 , . . . , gn }, and a disjoint finite set L of local program variables {l1 , l2 , . . . , lm }.
We denote by C the infinite set V \ (G ∪ L) of cut point variables ranged over by c1 , c2 , . . .. Further, we
assume a distinguished element nil ∈ G, used as a constant to refer to the undefined object. A Shylock
program acts only on global and local variables, cut point variables will be used later in the abstract
semantics as a kind of “freeze” variables for storing relevant points of the heap during procedure call.
For simplicity we assume that all objects have the same set of fields F = { f1 , . . . , fk }. We denote by
¯ c̄, f¯ the sequences of all global, local, cut point variables and fields, respectively.
ḡ, l,

102

Interacting via the Heap in the Presence of Recursion

For P a finite set of procedure names {p0 , . . . , pl }, a program is a set of procedure declarations of the
form pi :: Bi , where Bi , denoting the body of the procedure pi , is a statement defined by the following
grammar:
B ::= x. f := y | x := y. f | x := new | [x = y]B | [x 6= y]B | B + B | B; B | p
Here x and y are (local or global) program variables ranging over G ∪ L, f is a field in F and p is a
procedure name in P. We assume a distinguished p0 ∈ P, called the initial procedure of a program.
The assignment statements x. f := y or x := y. f assign the identity of the object referenced at right
hand side of the assignment to the field or variable, respectively, at the left hand side. The statement
x := new creates a new object that will be referenced by the program variable x. All fields of x will
reference the undefined object nil. We restrict to programs in which the variable nil does not appear
in the left-hand side of an assignment or object creation, i.e., nil is a constant. Conditional statements
[x = y]B and [x 6= y]B, nondeterministic choice B1 + B2 , and sequential composition B1 ; B2 , have the
standard interpretation. A procedure call p means that the body B associated with p is executed next
on the same global state but on a fresh local state. After the procedure body terminates, its local state
is destroyed forever and the previous local state (from which the procedure has been called) is restored.
Changes to the global state, however, remain.
Notice that variable assignment x := y. f and field update x. f := y suffice, as more general expressions and updates can be encoded. For example, a statement x := y. fi1 . . . fik is encoded as x := y. fi1 ; x :=
x. fi2 ; x := x. fi3 ; . . . ; x := x. fik . A basic variable assignment x := y can be encoded as z. f := y; x := z. f .
More general boolean expressions in conditional statements can be obtained by using sequential composition and nondeterministic choice. In fact (b1 ∧ b2 )B can be written as (b1 )b2 B, whereas (b1 ∨ b2 )B as
(b1 B) + (b2 B). Negation of a boolean expression b can be obtained by transforming b into an equivalent
boolean expression in conjunctive disjunctive normal form, for which negation of the simple expression
[x = y] and [x 6= y] is defined as expected. Ordinary while, skip, and if-then-else statements can be expressed easily in the language, using recursive procedures, conditional statements and nondeterministic
choice. For the sake of simplicity, we allow creation and assignment of a single object identity only; generalizations to simultaneous assignments and object creation can be added in a straightforward manner.
The language does not directly support parameter passing. However, it is worthwhile to note that we can
model procedures with call-by-value parameters by means of global variables. Let p(v1 , . . . , vn ) be a procedure with formal parameters v1 , . . . , vn . We see the formal parameters as local variables and introduce
for each parameter vi a corresponding global variable gi (which does not appear in the given program).
Every procedure call p(x1 , . . . , xn ) can then be encoded by the statement g1 := x1 ; . . . ; gn := xn ; p whereas
the body B of p(v1 , . . . , vn ) can be encoded by v1 := g1 ; . . . ; vn := gn ; B. A similar approach can be
taken to model procedures with return values. Finally, method calls x.m(x1 , . . . , xn ) can be modeled by
introducing the called object x as an additional parameter of the procedure m.
Example 1. We consider a simple example program which opens a file, passes it to some procedure
which returns again a file, and finally tries to close this returned file1 . It consists of the procedures main,
q, open and close, and the sets of global and local variables are G = {nil} and L = {x, y} respectively.
The procedures main, open and close are defined as follows:
main :: open(x); y := q(x); close(y)
open :: x := new
close(z) :: [z 6= nil]z := nil
1 This

idea was suggested to us by Dilian Gurov.

J. Rot, I.M. Asăvoae, F.S. de Boer, M.M. Bonsangue, D. Lucanu

103

The definition of q is left open. Recall from the above discussion that while parameter passing and return
values are not directly in the syntax of the language, they can easily be encoded. The intuition behind
this program is as follows. We start by executing main. Then first the program opens a file, modeled by
an object creation, and then it passes the reference x to this file on to a procedure q. This procedure q then
performs some calculations and passes back a file reference y. Finally we try to close the file referenced
by y. Closing a file is modeled by first checking if the given reference is not nil, and then simply setting
the reference to nil. If we pass close a reference to nil, then the program crashes.
In order to describe the formal semantics of Shylock programs, we first formalize some relevant
notions related to the heap. To represent object identities we use the set N⊥ = N ∪ {⊥} of natural
numbers extended with an element ⊥ and ranged over by n, m. Let s : V → N⊥ be a variable assignment
and h : F → (N⊥ → N⊥ ) be a field assignment such that for all f , h( f )(⊥) = ⊥ and the set of objects
for which h( f )(n) 6= ⊥ is finite. A heap H is a pair hs, hi of a variable- and a field assignment. We write
H(x) for s(x), and H( f ) for h( f ). For a subset of variables Var ⊆ V we denote with RH (Var) the set
of objects reachable from objects labeled by these variables in H via any of the (functional) transition
relations H( f ), for f ∈ F. Formally it is defined as the least fixpoint of the equation
RH (Var) = {H(x) | x ∈ Var} ∪ {H( f )(n) | f ∈ F, n ∈ RH (Var)}
If Var = V we denote the set of reachable objects of H by RH . Further we define the “purely local” part
of a heap H as RH = RH (L ∪C) \ RH (G). Intuitively RH contains all objects which are reachable from
a local (or cut point) variable, but not from a global variable.
We denote variable update by H[x := n], global field update by H[ f := ϕ] where ϕ : N⊥ → N⊥ is a
function such that ϕ(⊥) = ⊥, and local field update by H[ f := ϕ[n := m]]. We use the standard notation
and definition of simultaneous assignments and updates. A renaming ρ of a subset N ⊆ N⊥ is an injective
function in N⊥ → N⊥ such that ρ(n) = n for all n 6∈ N, and otherwise ρ(n) ∈ N. Clearly it has an inverse,
denoted by ρ −1 . Given a renaming ρ we define its application on a heap H as ρ(H)(x) = ρ(H(x)) and
ρ(H)( f )(n) = ρ(H( f )(ρ −1 (n))).
A configuration is a tuple hH, Γi where H is the current heap and Γ is a stack of statements and
heaps. The head of a stack is separated from the tail by means of the right-associative operator •, while
the empty stack is represented by ε. The current statement to be executed is on the top of the stack. When
there are no statements but an heap on the top of the stack, then a procedure returns, and the state on the
stack has to be restored as current state. A computation is a (possibly infinite) sequence C0 −→ C1 −→ . . .
of transitions, where −→ is a relation between configurations which we will now define by cases on the
top of the stack. To this end let Γ be a stack of statements and heaps. Assignments to a variable or to a
field update the current heap structure as expected:
hH, x := y. f • Γi −→ hH[x := H( f )(H(y))], Γi
hH, x. f := y • Γi −→ hH[ f := H( f )[H(x) := H(y)]], Γi
To model object creation we assume a distinguished global “system” variable oc which is used as a
counter, and does not appear in a program. We implicitly assume that H(oc) 6= ⊥, for every heap H. The
semantics of the operator “new” is:
hH, x := new • Γi −→ hH[x, oc := H(oc), H(oc) + 1][ f¯ := ϕ̄], Γi
where ϕ̄ is the sequence such that ϕi = H( fi )[H(x) := ⊥]. Conditional statements are executing depending on the evaluation of the condition:
H(x) = H(y)
hH, [x = y]B • Γi −→ hH, B • Γi

H(x) 6= H(y)
hH, [x 6= y]B • Γi −→ hH, B • Γi

104

Interacting via the Heap in the Presence of Recursion

Sequential composition adds on top of the stack the next statements to be executed, while nondeterministic choice selects just one of the two statements.
hH, B1 ; B2 • Γi −→ hH, B1 • B2 • Γi

hH, B1 + B2 • Γi −→ hH, Bi • Γi

i ∈ {0, 1}

Finally, procedure call and return are modeled as follows:
¯ B • H • Γi
hH, p • Γi −→ hH[l¯ := ⊥],

¯ Γi
hH, H 0 • Γi −→ hH[l¯ := H 0 (l)],

¯ denotes the pointwise application of H 0 to the local variables l,¯ and B is the body of the
where H 0 (l)
procedure p. Recall that for technical convenience there is a single sequence of local variables l¯ shared
by the procedures.
This section is concluded with the notion of properness, which is a formalization of some operational
properties of configurations appearing during the execution of programs. Suppose H and H 0 are heaps
which appear in the stack, meaning they are pending heaps from a procedure call, and H appears higher
up in the stack than H 0 (so H 0 was put on the stack before H). Then (1) the structure of the purely
local part of H 0 is preserved in H, since it could not have been accessed in between. Moreover (2) if
some object is reachable in both H and H 0 , then it must be reachable from a global variable in H 0 . Both
conditions intuitively capture the property that reachable objects remain reachable in a recursive call only
if they were already reachable from global variables.
Definition 1. The set of proper stacks is defined inductively as follows:
• the empty stack is proper
• if Γ is proper then B • Γ is proper for statements B
• if Γ is proper and H is a heap such that for every H 0 occurring in Γ the following holds:
– for all f ∈ F, n ∈ RH 0 : H( f )(n) = H 0 ( f )(n)
– RH 0 ∩ RH ⊆ RH 0 (G)
then H • Γ is proper.
A configuration hH, Γi is proper if H • Γ is a proper stack.
For example every configuration hH, p0 i is proper. Further, all transition steps preserve proper configurations. Thus every configuration in a computation starting from a proper one is proper.

3

Improving the semantics

The semantics introduced may generate, for a given program, a transition system with infinitely many
configurations. This is not only because of the unbounded stack size, but, more problematically, also
because each time a new object is allocated a new natural number is used. Thus, the number of heaps
needed is also unbounded. Consider for example the Shylock program consisting of a single procedure
p with as body the statement
x := new; p
where x is a local variable. Each time the statement x := new is executed, a new natural number is
assigned to x. This has the unfortunate consequence that infinitely many heaps are needed, and thus
the usual model checking techniques for recursive systems [10, 21] cannot be guaranteed to terminate.
In this section we introduce an abstract semantics for Shylock, based on reuse of natural numbers for

J. Rot, I.M. Asăvoae, F.S. de Boer, M.M. Bonsangue, D. Lucanu

105

objects. Identities of objects that are not in use in the current heap will be reused instead of using a new
identity each time a new object is allocated. More concretely, when creating a new object we will choose
the minimal unused identity available, as formally expressed by the following rule:
hH, x := new • Γi −→ hH[x := n][ f¯ := ϕ̄], Γi
where n = min(N \ RH ), and, for each i, ϕi = H( fi )[n := ⊥]. The intuition here is that numbers are no
longer concrete object identities, but instead they represent equivalence classes. However, this adapted
rule may introduce name clashes with objects in the local state pending on the stack. We illustrate this
problem and our solution with an example. Consider the following heap:
f

l:0

f


/ nil : ⊥

f

/ g:1

Here x : n represents the identity n to which the variable x refers (so technically the figure represents a
heap H for which H(l) = 0, H( f )(0) = 1, etc.). Further l is a local variable, g is a global variable, and
f is the single field. Let us consider first the execution of a call to a procedure p :: g := new. Starting
from the above heap, on the call a copy is placed onto the stack and the local variable l is initialized to
⊥, so the procedure p is executed on the following heap:
f
f

g:1



/ l, nil : ⊥

When executing g := new we take for g the minimal object identity unreachable from the current variables, which is 0. Then, on procedure return, we see that there is a name clash: both g and l point to the
object with identity 0, while they should obviously not be identified. A solution is to rename the object
n to which g points, i.e., to make g point to an identity m which is used neither by the current nor the
caller’s stored heap, and updating the fields of this new object according to the fields of n. Then we can
just take the union of the global part of the new heap, and the local part of the stored heap. For example
we could rename, in the current heap, the object 1 to 2, which is free, take the union with the (local part
of the) stored heap of the caller, and combine the two heaps as follows:
f

l:0

f

/ 1

f


/ nil : ⊥ o f

g:2

However, consider now the execution of a procedure p0 :: g := new; g := new, starting from the same
heap as before (the first figure above). After executing the first object creation statement in the procedure,
g again points to 0. But then after the second time we execute g := new, g is assigned the minimal index
available, which is 1 at that point. Thus on procedure return, the heap is exactly the same as in the
beginning of the procedure execution. So two object creations are in this case indistinguishable from no
creation at all. On the procedure return, when combining the current heap with the stored heap it is thus
not clear whether g should keep pointing to 1 (when no object creation statements were executed), or if it
should be renamed to a new identity separate from the others (when two object creation statements were
executed).

106

Interacting via the Heap in the Presence of Recursion

Our solution to this problem is a non-trivial extension of the semantics of procedure call and -return
based on the identification of so-called cut points, which are the object identities at the “edge” of the
global and the local part of the heap, representing exactly the point where the local part “enters” the
global part. On a procedure call, these cut points are identified, and we assign their values to a set of
distinguished cut point variables, in the heap of the callee. Then, on procedure return, the cut point
variables “connect” the current heap with the stored one, giving us precisely the information about how
to combine the two. Returning to our example, consider the following heap:
f

g, c : 1

f



/ l, nil : ⊥

This heap represents the initial heap of the callee, extended with the only cut point of the caller heap, in
the form of the cut point variable c. Now if we execute g := new; g := new, the global variable g is not
assigned the identity 1 since it is already in use. So now on procedure return we can distinguish between
the case that g was newly created (in which case it will have a new identity), and the case that it was not
(in which case it will have the same identity as before).
Formally, for a given heap H, the set CPH of cut points is defined as follows:
RH (G) ∩ (H(L ∪C) ∪ F(RH ))
where F(N) = {H( f )(n) | n ∈ N, f ∈ F}. Further, H(V ) means applying H point-wise to V , hence
H(L ∪C) = {H(v) | v ∈ L ∪C}. Note that the definition involves the cut point variables; recall from the
above discussion that these variables represent the cut points of the previous heap. Further recall that
RH (G) is the global part of the heap, while RH is the “purely local” part of the heap. Intuitively, F(RH )
represents the objects which are pointed to by a field from an object which is purely local. Further
H(L ∪C) ∩ RH (G) is the set containing objects pointed to directly by the local variables, which are also
reachable from global variables. On the other hand, F(RH ) ∩ RH (G) contains objects adjacent to the
purely local (reachable) nodes (where the node adjacency is provided by the field transitions).
Now the procedure call of the improved semantics is modeled by the following rule.
¯ c̄ := n̄], Bi • H • Γi ,
hH, pi • Γi −→ hH[v̄ := ⊥][
where v̄ is the sequence of local variables and cut point variables c for which H(c) 6= ⊥. Further c̄ is a
sequence of cut point variables of the same length as the sequence n̄ of cut points CPH . Note that, given
a heap Hc , if on top of the stack we have a heap Hl , by the way we modeled the procedure call, the cut
points in the stacked heap Hl correspond exactly to the cut point variables in the current heap Hc .
We proceed to discuss the construction of the return heap, say Hr . We first rename all objects of the
purely local part of Hl which conflict with Hc , meaning that they are also reachable from global variables
in Hc . When this is done, we can just copy all the local variables directly to Hc and update the fields of
the purely local part of Hl in Hc . In order to formalize this process we define the set of name clashes N
of Hc and Hl :
N = RH l ∩ RHc (G)
Remember that RH l only contains the objects which are reachable from a local variable (or from a
previous cut point variable), and are not reachable from any global variable. Now the return rule is
formalized as follows:
hHc , Hl • Γi −→ hθ ◦ ρ(Hc ), Γi
where

J. Rot, I.M. Asăvoae, F.S. de Boer, M.M. Bonsangue, D. Lucanu

107

• ρ is a renaming, monotonic on N, such that ρ(n) ∈ N\RHc [l¯ := ⊥]
¯ if n ∈ N, and ρ(n) = n otherwise,
and ρ is minimal w.r.t pointwise comparison between renaming functions
• θ resets the purely local part:
¯ c̄ := Hl (l),
¯ Hl (c̄)][ f¯ := ϕ̄]
θ (H) = H[l,
where c̄ is the sequence of cut point variables c for which Hl (c) 6= ⊥, and ϕ̄ is the sequence defined,
for all n ∈ N⊥ , as follows:
(
Hl ( fi )(n) if n ∈ RH l
ϕi (n) :=
Hc ( fi )(n) otherwise
Correctness We provide a proof of the equivalence between the concrete semantics of Shylock, and
the abstract semantics defined in the previous section. To this end we adapt the concrete semantics to take
into account the initialization and restoration of the cut point variables, similar to the abstract semantics.
Note that this does not affect the behaviour of programs, as they are assumed not to contain cut point
variables. First we need the basic notion of heap isomorphism:
Definition 2. Two heaps H and H 0 are isomorphic, denoted H ∼ H 0 , if there exists a function α : RH →
RH 0 such that
• α is a bijection.
• For each x ∈ V : α(H(x)) = H 0 (x).
• For each f ∈ F and n ∈ RH : α(H( f )(n)) = H 0 ( f )(α(n)).
Note that since fields are deterministic, such a function α, if it exists, is unique. In order to proceed,
we introduce the important notion of cut point identification. Recall that on a procedure call, the new
heap Hc represents in its cut point variables the cut points of the caller heap Hl . Suppose now we
have other heaps Hc0 and Hl0 such that Hc ∼ Hc0 and Hl ∼ Hl0 . Note that cut points are preserved by
isomorphisms. Cut point identification now formalizes the representation of cut points of Hl and Hl0 in
Hc and Hc0 respectively, using for each cut point in Hl and Hl0 the same variable to represent it in Hc and
Hc0 .
Definition 3 (Cut point identification). Let Hc , Hl , Hc0 , Hl0 be heaps such that Hc ∼αc Hc0 , Hl ∼αl Hl0 . Let
{n1 , . . . , nk } = CPHl be the cut points of Hl . We define
(Hc , Hl ) ./ (Hc0 , Hl0 )
iff there exists a sequence of cut point variables c1 , . . . , ck such that for all i ≤ k:
Hc (ci ) = ni and Hc0 (ci ) = αl (ni )
From this definition we immediately deduce that the two isomorphisms agree on cut points:
Corollary 1. If (Hc , Hl ) ./ (Hc0 , Hl0 ) then for all n ∈ CPHl : αl (n) = αc (n).
Proof. For all ni ∈ CPHl we have αl (ni ) = Hc0 (ci ) = αc (Hc (ci )) = αc (ni ).
Now we are ready to introduce a strong notion of equivalence, based on heap isomorphism, which
also takes along the main operational properties characterizing configurations appearing in computations.
Definition 4. Given stacks Γ, Γ0 we define Γ ∼ Γ0 inductively as follows:

108

Interacting via the Heap in the Presence of Recursion
• if Γ and Γ0 are both empty then Γ ∼ Γ0
• if Γ ∼ Γ0 then B • Γ ∼ B • Γ0
• if
– Γ ∼ Γ0 , H ∼ H 0
– (H, ν(Γ)) ./ (H 0 , ν(Γ0 ))
– H • Γ is proper
then H • Γ ∼ H 0 • Γ0

where ν(Γ) extracts from the stack the top heap. Now for configurations we define hH, Γi ∼ hH 0 , Γ0 i iff
H • Γ ∼ H 0 • Γ0 .
The following lemma states how the current heap and the stacked heap are combined on a procedure
return in the concrete semantics. More precisely it expresses that any identity which becomes reachable
right after a procedure returns, is in the purely local part of the heap of the caller procedure.
¯
Lemma 1. Suppose hHc , Hl • Γi ∼ hHc0 , Hl0 • Γ0 i. Let Hr = Hc [l¯ := Hl (l)].
Then for all n ∈ RHr : if

n 6∈ RHc (G ∪C) then n ∈ RHl .
Proof. Let Hc , Hl , Hr be as above. Let n ∈ RHr and assume n 6∈ RHc (G ∪C), so n is reachable in Hr from
a local variable. We prove by induction that any path in Hr reaching such an n is reflected in the same
path in Hl which lies entirely in its purely local part RH l .
¯
Suppose first that n = Hr (l) for some local variable l. Then n = Hr (l) = Hc [l¯ := Hl (l)](l)
= Hl (l).
Now by assumption (that is in the relation ∼), Hc has cut point variables precisely on the cut points of
Hl . We may then conclude that n is not reachable from a global variable in Hl ; otherwise it would, by
definition (of cut points) be on a cut point of Hl , and consequently on a cut point variable in Hc which
contradicts our assumption on the reachability of n. Thus n ∈ RH l .
Now let n = Hr ( fi ) ◦ . . . ◦ Hr ( f1 )(Hr (l)) such that n 6∈ RHc (G ∪ C), n = Hl ( fi ) ◦ . . . ◦ Hl ( f1 )(Hl (l))
and n ∈ RH l . Suppose Hr ( f )(n) 6∈ RHr (G ∪C) for some field f . Since n ∈ RH l and Hc • Hl is proper we
have Hl ( f )(n) = Hr ( f )(n). Now Hr ( f )(n) 6= Hc (c) for all cut point variables c; otherwise n would be
reachable from such an Hc (c) which would be a contradiction with our assumption. But then by the cut
point identification of Hc and Hl , Hl ( f )(n) is not on a cut point of Hl , which implies that the global state
has not been entered yet, i.e., Hl ( f )(n) ∈ RH l as desired.
We are now ready for the main theorem of this section, stating that the concrete and the abstract
semantics are equivalent.
Theorem 1 (Bisimulation). Let C1 and C2 be configurations such that C1 ∼ C2 . Denote with →c and
→a the transition relations corresponding to the concrete and the abstract semantics, respectively. If
C1 →c C10 then there exists a configuration C20 such that C2 →a C20 and C10 ∼ C20 , and vice versa.
Proof. We only discuss the isomorphism of the resulting heaps on procedure return. Suppose
hHc , Hl • Γi ∼ hHc0 , Hl0 • Γ0 i
By definition of the concrete and the abstract semantics from these respective configurations the enabled
transitions are
hHc , Hl • Γi →c hHr , Γi and hHc0 , Hl0 • Γ0 i →a hHr0 , Γ0 i

J. Rot, I.M. Asăvoae, F.S. de Boer, M.M. Bonsangue, D. Lucanu

109

where Hr0 = θ ◦ρ(Hc0 ). By definition of ∼ there are isomorphisms Hc ∼αc Hc0 and Hl ∼αl Hl0 . We explicitly
define an isomorphism α : RHr → RHr0 as follows:
(
ρ ◦ αc (n)
α(n) =
αl (n)

if n ∈ RHc (G ∪C)
otherwise

Note that by Lemma 1, if n 6∈ RHc (G ∪ C) then n ∈ RH l so α is well-defined. To see that α is an
isomorphism, intuitively, note that αc is an isomorphism on RHc (G ∪ C) and αl is an isomorphism on
RH l , and by cut point identification we known from Corollary 1 that αc (n) = αl (n) for all n ∈ CPHl .

4

Model checking Shylock programs

In this section we present a framework for model checking Shylock programs. We first turn our abstract
semantics into a pushdown system, then we introduce a linear time temporal logic for heap structures,
and finally we shortly recall the actual model checking procedure.
Programs as pushdown systems A pushdown system can be considered as a pushdown automaton
without an input alphabet. Formally a pushdown system P is a triple (∆, Σ, 7→) where ∆ is a set of
control locations, Σ is a stack alphabet, and 7→ is a subset of h∆ × Σi × h∆ × Σ∗ i representing the set of
rules. A pushdown system is said to be finite when the above three sets are all finite.
The behaviour of any Shylock program P = {p0 :: B0 , . . . , pl :: Bl } can be represented by a pushdown system PP = (∆, Σ, 7→), where ∆ is the set of all heaps, and Σ = ∆ ∪ cl(P) ∪ {Z}, where Z is an
element which does not occur in ∆ and cl(P). Here cl(P) is the set of all possibly reachable statements
in P, and it is defined as the union of all cl(Bi ), for all 0 ≤ i ≤ l, with cl(B) given inductively by:
cl(x. f := y) = {x. f := y}
cl(x := new) = {x := new}
cl([x = y]B) = {[x = y]B} ∪ cl(B)
cl(B1 + B2 ) = cl(B1 ) ∪ cl(B2 ) ∪ {B1 + B2 }

cl(x := y. f ) = {x := y. f }
cl(p) = {p}
cl([x 6= y]B) = {[x 6= y]B} ∪ cl(B)
cl(B1 ; B2 ) = cl(B1 ) ∪ cl(B2 )

The rules of the pushdown system are specified using the abstract semantics as follows:
hH, γi 7→ hH 0 , wi

iff

hH, γ • Γi −→ hH 0 , w • Γi

where H ranges over heaps. Further we add rules hH, γi 7→ hH, Zi for any configuration hH, γi which
does not have outgoing transitions to complete with stuttering steps terminating computations starting
from hH0 , p0 • Zi. Because there are infinitely many heaps, the pushdown system constructed above will
in general be infinite. Consequently existing model checking techniques can not be applied. In order to
allow model checking we consider a subclass of programs. First, we need the following definition:
Definition 5. A heap H is k-bounded if |RH (G ∪ L)| ≤ k. A computation hH0 , Γ0 i → hH1 , Γ1 i → . . .
(where the transition steps are according to the abstract semantics) is k-bounded if |RHi | is k-bounded
for all i. A program P with main procedure p0 is k-bounded if every computation hH, p0 i → . . . is
k-bounded.
Example 2. As an example of a program which is bounded in this sense, recall the program with a single
procedure defined as p :: x := new; p, where x is a local variable. Indeed only one object identity is

110

Interacting via the Heap in the Presence of Recursion

needed to represent the object to which x refers, so this program is 1-bounded. Nevertheless, since x is
local, during the execution of the program an unbounded number of objects are stored on the stack.
For another example, recall the program from Example 1 which opens and closes a file. This program
is k-bounded iff the visible heap during execution of the procedure q(x) (with x a fresh object) is kbounded.
Now if we restrict to k-bounded programs, the abstract semantics, because of its reuse of object
identities, allows us to represent the behaviour of a program as a pushdown system as above, but using
as control states only k-bounded heaps. By Theorem 1, we then have precise abstractions of k-bounded
programs as finite pushdown systems. More precisely, given a k-bounded program P we define the
pushdown system k-PP = (∆k , Σk , 7→k ) obtained as a restriction from PP as follows. First, ∆k = {H |
|RH (G ∪ L)| ≤ k} ∪ {>} is the subset of all k-bounded heaps. The stack alphabet Σk is given by ∆k ∪
cl(P) ∪ {Z}, and the relation 7→k is the restriction of 7→ to ∆k together with the two out-of-bound rules
below
hH, γi 7→ hH 0 , wi |RH 0 | > k
and h>, γi 7→k h>, γi
hH, γi 7→k h>, γi
Note that in fact for any program P, k-PP is a finite pushdown system. However it is a precise abstraction
of P only if P is k-bounded.
Specifications in Li Tt Le In order to do a precise pointer analysis of Shylock programs, we introduce a
linear time temporal logic (Li Tt Le ) for describing the evolution of the heap structure. We first introduce
the language of the properties satisfied by a given heap, which will form the atomic properties of the
linear temporal logic. We do so by the introduction of expressions of the Kleene algebra with tests [13]
over fields and variables. More precisely, let Rite be the smallest set defined by the following grammar:
r ::= ε | x | ¬x | f | r.r | r + r | r∗
where x ranges over variable names (to be used as tests) and f over field names (to be used as actions).
The regular expressions introduced by Rite are similar to the heap patterns used in matching logic [20]
r
and separation logic [18]. We define a transition relation n →
− H m between objects of a heap H as the
least relation such that
ε

n→
−H n
x
n→
−H n
¬x
n −→H n

if H(x) = n
if H(x) 6= n

f

n→
−H m
if H( f )(n) = m
r1 +r2
r1
r2
n −−−→H m if n −
→
m or n −
→
m
r1 .r2
r1
r2
0
0 →
n −−→H m if exists an object n0 such that n −
→
H n and n −
H m
r∗

n−
→H m

r

r∗

if either n = m or there exists an object n0 such that n →
− H n0 and n0 −
→H m

Further we introduce the following modal interpretation of regular expressions:
r

H |= r if and only if for each reachable object n ∈ RH there exists m such that n →
− H m.
(Note that this coincides with the truth definition of H |= hritrue in dynamic logic.) For instance, the
regular expression first.next∗ .last + ¬first is satisfied by a heap H if and only if the object referred to by

J. Rot, I.M. Asăvoae, F.S. de Boer, M.M. Bonsangue, D. Lucanu

111

the variable first is linked via a chain of fields next with the object referred to by the variable last, or first
is not allocated.
Our Li Tt Le formulas are built according to the following grammar:
φ ::= true | r | ¬φ | φ1 ∧ φ2 | Xφ | φ1 Uφ2
where r ranges over Rite. Other propositional connectives ∨, → are defined in terms of ∧ and ¬. Further
we define Fφ = true U φ and Gφ = ¬F(¬φ ). We define At(φ ) to be the set of atomic propositions r ∈ Rite
which appear in φ . Clearly At(φ ) is always a finite set.
For a set X we denote its powerset by 2X . With (2At(φ ) )ω = {w0 w1 w2 . . . |wi ∈ 2At(φ ) for all i ≥ 0}
we denote the set of infinite words over sets of expressions in At(Φ). Given such an infinite word
w = w0 w1 w2 . . . we denote with wi the i-th element, and with w[i . . .] the subsequence wi wi+1 . . . starting
from the i-th element of w. For a Li Tt Le formula φ and an infinite word w ∈ (2At(φ ) )ω we denote that w
satisfies φ by w |= φ . This satisfaction relation is defined inductively on the structure of φ according to
the standard semantics of LTL [1]:
w |= true
w |= r
w |= φ1 ∧ φ2
w |= ¬φ
w |= Xφ
w |= φ1Uφ2

iff r ∈ w
iff w |= φ1 and w |= φ2
iff w 6|= φ
iff w[1 . . .] |= φ
iff ∃ j ≥ 0.w[ j . . .] |= φ2 and w[i . . .] |= φ1 for all 0 ≤ i < j

Let π be an infinite sequence of k-bounded heaps for some k, i.e., π ∈ {H0 H1 H2 . . . |Hi ∈ ∆k for all i ≥ 0}.
Intuitively, π represents a trace of heaps which we encounter during a particular computation of a kbounded program. We say that π |= φ if and only if there exists a sequence w ∈ (2At(φ ) )ω such that
w |= φ and for all i ≥ 0:
πi |= r for all r ∈ wi
Finally the above relation |= is pointwise extended to sets of infinite sequences of k-bounded heaps.
Model checking Recall that a Büchi automaton B = (∇, A, , Q0 , F) consists of a finite set of states
∇, an input alphabet A, a transition relation ⊆ ∇ × A → ∇, a set of initial states Q0 and a set of final
states F. The language L (B) accepted by B is the set of all infinite words w over A such that there is
an infinite path via
labeled by w, starting from a state q0 ∈ Q0 , and visiting an accepting state in F
infinitely often. Given a Li Tt Le formula φ , one can effectively construct a Büchi automaton Bφ which
recognizes exactly the set of words w over sets of expressions in At(φ ) satisfying φ (see e.g. [1] for
details).
Let φ be a formula of our temporal logic for heaps, and P be a k-bounded Shylock program. To
check if P satisfies the formula φ , we have to check if all the computations of the pushdown system
k-PP starting from the initial configuration hH0 , p0 • Zi satisfy φ . This amounts to synchronizing the
pushdown system k-PP with the Büchi automaton B¬φ and checking if the resulting Büchi pushdown
system has an accepting run, i.e., a run starting from the initial states of the two systems which visits
infinitely often configurations whose control locations projected into the states of the Büchi automaton
are final [10, 21].
The problem of finding an accepting run of a Büchi pushdown system can be reduced to that of
finding a repeated head reachable from the initial configuration [10, 21]. Computing the repeating heads

112

Interacting via the Heap in the Presence of Recursion

is typically developed in two phases. In the first phase, one constructs the head reachability graph G
associated with a Büchi pushdown system, while in the second phase, G is analyzed to identify those
nodes of the graph which are repeated heads. To avoid redundant computations, it suffices to construct
the head reachability graph G restricted to those configurations reachable from an initial configuration
of the Büchi pushdown system. This can be done using forward reachability analysis, by using the so
called post∗ method. For more details, see, e.g., Chapter 3 in [21].
Shylock and [4] As discussed in the introduction, the related work closest to our approach is presented
in [4]. While [4] considers only reachability, this could be extended to a full model checking procedure
along the lines discussed in this paper. A first view on the two works shows that [4] has a very high level
solution to the problem while we give an explicit solution to it. The semantics of procedure call and
specifically of the procedure return as given in [4] are stated in terms of abstract graph isomorphisms,
and it is not clear how they should be implemented. In contrast, in this paper we give a purely symbolic
characterization of procedure call and return.
Now we present a more detailed view on the difference between the semantics given in the two
works. The procedure call in [4] employs the cut point mechanism as well, but it also cleans the heap of
the currently unreachable objects. Hence, their procedure call passes to the callee only the strictly visible
heap of the caller, actually an isomorphic instance of it. In contrast, Shylock’s procedure call relies on
the cut points as well, but it doesn’t necessarily clean the heap (though it could). Instead, Shylock reuses
object identities on demand, during the object creation statements of the procedure, while [4] doesn’t pay
attention to the body of the procedure because of the initial cleaning. Though Shylock may seem lazy
w.r.t. cleaning, it’s memory reuse mechanism acts in fact as a localized cleaning. This pays off during
the execution of the procedure returns. Namely, in [4] the procedure return has to proceed by renaming
the entire visible object space, such that it can synchronize the current heap with the caller’s heap.
Meanwhile, Shylock renames only the name clashes, i.e., the objects at the intersection of the caller’s
global heap and the callee’s current purely local heap. These differences induce a different reasoning
during the verification phase. Namely, while Shylock can afford to use heap equality during the model
checking phase, the reachability procedure in [4] has to be performed on normal forms of the heaps (i.e.,
on the representatives of the graph isomorphic equivalence class). We are not sure if Shylock maintains
strictly one representative of each isomorphic class, but we plan to study this particular aspect in the near
future.

5

Conclusions

In the presence of recursive procedures and local variables, an unbounded number of objects can be
allocated either on the call stack using local variables, or, anonymously, on the heap using reference
fields. In this paper we discussed Shylock, a language which supports these features, together with
a formal abstract semantics which allows model checking in the context of bounded visible heaps. We
introduced a temporal logic for specifying properties of the heap, and discussed a procedure for checking
these properties against Shylock programs.
Future work Shylock’s improved semantics has been implemented in the K framework. We are currently implementing a general model checking technique for recursive programs defined in K, from
which we would obtain a Shylock model checker along the lines described in this paper. Further we are
investigating the expressive power of programs with a bounded visible heap.

J. Rot, I.M. Asăvoae, F.S. de Boer, M.M. Bonsangue, D. Lucanu

113

References
[1] C. Baier and J.-P. Katoen. Principles of Model Checking The MIT press, 2008.
[2] J. Berdine, C. Calcagno, and P. O’Hearn. A decidable fragment of separation logic. In FSTTCS ’04, pp.
97–109. Springer, 2004. doi:10.1007/978-3-540-30538-5 9
[3] F. S. de Boer, M. M. Bonsangue, J. Rot. Automated Verification of Recursive Programs with Pointers. In
Proc. IJCAR ’12, vol. 7364 of LNAI, Springer, 2012. doi:10.1007/978-3-642-31365-3 14
[4] A. Bouajjani, S. Fratani, S. Qadeer. Context-Bounded Analysis of Multithreaded Programs with Dynamic
Linked Structures. In Proc. of CAV 2007 vol. 4590 of LNCS, pp. 207–220. Springer, 2007. doi:10.1007/9783-540-73368-3 24
[5] V. Ciancia and U. Montanari. Symmetries, local names and dynamic (de)-allocation of names. In Information
and Computation 28(12): 1349 - 1367, 2010. doi:10.1016/j.ic.2009.10.007
[6] J. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pǎsăreanu, Robby, and H. Zheng. Bandera: Extracting
finite-state models from java source code. In Proc. 22nd International Conference on Software Engineering,
pp. 439–448. IEEE, 2000. doi:10.1109/ICSE.2000.870434
[7] M. Dam. Model checking mobile processes.
doi:10.1006/inco.1996.0072

In Information and Computation, 121(1):35–51, 1996.

[8] C. Demartini, R. Iosif, and R. Sisto.
A deadlock detection tool for concurrent java programs. In Software - Practice and Experience, vol. 29, pp. 577–603, 1999. doi:10.1002/(SICI)1097024X(199906)29:7¡577::AID-SPE246¿3.0.CO;2-V
[9] D. Distefano, J.-P. Katoen, and A. Rensink. Who is pointing when to whom? In Proc. of Foundations of
Software Technology and Theoretical Computer Science (FSTTCS 2004), vol. 3328 of LNCS, pp. 250–262.
Springer, 2004. doi:10.1007/978-3-540-30538-5 21
[10] J. Esparza and S. Schwoon. A bdd-based model checker for recursive programs. In Proc. of CAV 2001, vol.
2102 of LNCS, pp. 324–336. Springer, 2001. doi:10.1007/3-540-44585-4 30
[11] A. Finkel, E. Lozes, and A. Sangnier. Towards model-checking programs with lists. Infinity in Logic and
Computation, volume 5489 of LNAI, pp. 56–86. Springer, 2009. doi:10.1007/978-3-642-03092-5 6
[12] K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. In International
Journal on Software Tools for Technology Transfer, 2:366–381, 2000. doi:10.1007/s100090050043
[13] D. Kozen.
Kleene algebra with tests.
ACM Trans. Program. Lang. Syst., 19:427–443, 1997.
doi:10.1145/256167.256195
[14] S. Labbe, and A. Sangnier. Formal verification of industrial software with dynamic memory management.
PRDC ’10, pp. 77–84. IEEE Computer Society, 2009. doi:10.1109/PRDC.2010.19
[15] P. Madhusudan, G. Parlato, and X. Qiu. Decidable logics combining heap structures and data. In POPL ’11,
pp. 611–622. ACM, 2011. doi:10.1145/1926385.1926455
[16] U. Montanari and M. Pistore. An introduction to history-dependent automata. In Electronic Notes in Theoretical Computer Science 10:170–188, 1997. doi:10.1016/S1571-0661(05)80696-6
[17] D. Park, U. Stern, J. Skakkebaek, and D. Dill. Java model checking. In Proc. of the 15th IEEE Int. Conf. on
Automated Software Engineering, pp. 253–256. IEEE, 2000. doi:10.1109/ASE.2000.873671
[18] J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS ’02, pp. 55–74. IEEE,
2002. doi:10.1109/LICS.2002.1029817
[19] N. Rinetzky, J. Bauer, T. W. Reps, S. Sagiv, and R. Wilhelm. A semantics for procedure local heaps and its
abstractions. In POPL 2005, pp. 296–309, 2005. doi:10.1145/1040305.1040330
[20] G. Roşu, C. Ellison and W. Schulte. Matching Logic: An Alternative to Hoare/Floyd Logic. In AMAST ’10,
vol. 6486 of LNCS, pp. 142-162. Springer, 2010. doi:10.1007/978-3-642-17796-5 9
[21] S. Schwoon. Model-Checking Pushdown Systems. PhD thesis, Technische Universität München, 2002.

