Test input generation with java PathFinder.
We show how model checking and symbolic execution can be used to generate test inputs to achieve structural coverage of code that manipulates complex data structures. We focus on obtaining branch-coverage during unit testing of some of the core methods of the red-black tree implementation in the Java TreeMap library, using the Java PathFinder model checker. Three different test generation techniques will be introduced and compared, namely, straight model checking of the code, model checking used in a black-box fashion to generate all inputs up to a fixed size, and lastly, model checking used during white-box test input generation. The main contribution of this work is to show how efficient white-box test input generation can be done for code manipulating complex data, taking into account complex method preconditions.
We evaluate our approaches by generating tests for the
red-black tree [16] implementation in the Java TreeMap li-
brary. The contributions of our work are:
A powerful and exible test input generation frame-work
for unit testing. The framework uses an ecient
approach to the symbolic execution of code manipulating
complex data structures, that takes into account
preconditions to stop the analysis of infeasible paths
as soon as possible. The framework can be used uniformly
both for white-box and black-box testing.
We show how our framework can be used for generating
tests for code manipulating complex data structures
specically red-black trees.
We illustrate the exibility of model checking as a tool
for test input creation by comparing straight model
checking of the code under test, a black-box approach
and a white-box approach.
2. BACKGROUND
We describe here the Java PathFinder (JPF) model checker
[43] that has been extended with a symbolic execution ca-
x: X, y: Y
PC: true
x: X, y: Y
PC: X>Y
x: X, y: Y
PC: X<=Y
x: X+Y, y: Y
PC: X>Yint x,
1:if {
2:
3:
4:
5: if (x > y)
x: X+Y, y: X
PC: X>Y
x: Y, y: X
PC: X>Y
x: Y, y: X
x: Y, y: X

Figure

1: Code that swaps two integers and the corresponding
execution tree, where transitions
are labelled with program control points
pability. We show in Section 4 how we use this extension of
JPF for white-box and black-box test input generation.
2.1 Java PathFinder
JPF is an explicit-state model checker for Java programs
that is built on top of a custom-made Java Virtual Machine
(JVM). JPF can handle all of the language features of Java
and it also treats nondeterministic choice expressed in annotations
of the program being analyzed | annotations are
added to the programs through method calls to a special
class Verify. The following methods from the Verify class
will be used in this paper:
randomBool() returns a boolean value nondeterministically.
random(n) returns values [0; n] nondeterministically.
ignoreIf(cond) forces the model checker to backtrack when
cond evaluates to true.
JPF has previously been used to nd errors in a number
of complex systems including the real-time operating system
DEOS from Honeywell [39] and a prototype Mars Rover
developed at NASA Ames (called K9) [11]. More recently
it was also used as a means for generating input plans that
the current K9 rover takes as input [5] | the plans were
generated in a black-box fashion similar to the technique
described in section 4.2.
2.2 Symbolic Execution in Java PathFinder
In this section we give some background on symbolic execution
and we present the symbolic execution framework
used for reasoning about Java programs.
2.2.1 Background: Symbolic Execution
The main idea behind symbolic execution [31] is to use
values, instead of actual data, as input values and
to represent the values of program variables as symbolic ex-
pressions. As a result, the outputs computed by a program
are expressed as a function of the symbolic inputs.
The state of a symbolically executed program includes the
(symbolic) values of program variables, a path condition (PC)
and a program counter. The path condition is a (quantier
over the symbolic inputs; it accumulates
constraints which the inputs must satisfy in order for
an execution to follow the particular associated path. The
program counter denes the next statement to be executed.
A symbolic execution tree characterizes the execution paths
followed during the symbolic execution of a program. The
nodes represent program states and the arcs represent transitions
between states.
Consider the code fragment in Figure 1, which swaps the
values of integer variables x and y, when x is greater than y.

Figure

also shows the corresponding symbolic execution
tree. Initially, PC is true and x and y have symbolic values X
and Y, respectively. At each branch point, PC is updated with
assumptions about the inputs, in order to choose between
alternative paths. For example, after the execution of the
rst statement, both then and else alternatives of the if
statement are possible, and PC is updated accordingly. If
the path condition becomes false, i.e. there is no set of
inputs that satisfy it, this means that the symbolic state is
not reachable, and symbolic execution does not continue for
that path. For example, statement (6) is unreachable.
2.2.2 Generalized Symbolic Execution
In [30] we describe an algorithm for generalizing traditional
symbolic execution to support advanced constructs
of modern programming languages, such as Java and C++.
The algorithm handles dynamically allocated structures, primitive
data and concurrency. We have since extended the
work in [30] by adding support for symbolic execution of
arrays.
The algorithm starts execution of a method on inputs with
uninitialized elds and uses lazy initialization to assign values
to these elds, i.e. it initializes elds when they are rst
accessed during the method's symbolic execution. This allows
symbolic execution of methods without requiring an a
priori bound on the number of input objects.
When the execution accesses an uninitialized reference
eld, the algorithm nondeterministically initializes the eld
to null, to a reference to a new object with uninitialized
elds, or to a reference of an object created during a prior
eld initialization; this systematically treats aliasing. When
the execution accesses an uninitialized primitive (or string)
eld, the algorithm rst initializes the eld to a new symbolic
value of the appropriate type and then the execution
proceeds.
When a branching condition on primitive elds is eval-
uated, the algorithm nondeterministically adds the condition
or its negation to the corresponding path condition
and checks the path condition's satisability using a decision
procedure. If the path condition becomes infeasible,
the current execution terminates (i.e. the algorithm back-
tracks).
2.2.3 Framework
Our symbolic execution framework is built on top of the
JPF model checker. To enable JPF to perform symbolic
execution (and lazy initialization), the original program is
instrumented by doing a source to source translation that
adds nondeterminism and support for manipulating formulas
that represent path conditions1.
1The interested reader is referred to [30] for a detailed description
of the code instrumentation
class Node {
int elem;
Node next;
/* precondition: acyclic()
void foo() { .
1: if (elem > t.elem)
2:
*/

Figure

2: Simple example to illustrate generalized
execution
The model checker checks the instrumented program using
its usual state space exploration techniques | essentially,
the model checker explores the symbolic execution tree of
the program. A state includes a heap conguration, a path
condition on primitive elds, and thread scheduling. Whenever
a path condition is updated, it is checked for satisability
using an appropriate decision procedure, such as the
Omega library [40] for linear integer constraints. If the path
condition is unsatisable, the model checker backtracks.
The framework can be used for test input generation and
for nding counterexamples to safety properties. For test
input generation, the model checker generates paths that are
witnesses to a testing criterion encoded as a set of properties.
For every reported path, the model checker also reports the
input heap conguration (encoding constraints on reference
elds), the path condition for the primitive input elds, and
thread scheduling, which can be used to reproduce the error.
Note that performing (forward) symbolic execution on
programs with loops can explore innite execution trees.
This is why, for systematic state space exploration, the frame-work
uses depth rst search with iterative deepening or
breadth rst search.
Although we concentrate in this paper on the analysis
of sequential code, it is worth mentioning that our symbolic
execution framework handles concurrency, as it uses
the model checker to systematically analyze thread inter-
leavings. Using a model checker as a search engine for our
framework allows us to also exploit other built-in capabilities
of the model checker, such as backtracking, dierent
search capabilities (e.g. heuristic search), and techniques
that combat state-explosion (e.g. partial order and symmetry
reductions). We should also note that, although we
consider here branch coverage as a metric for testing, our
framework can handle other testing criteria that can be encoded
as properties the model checker should check for (e.g.
data-ow based coverage).
2.2.4 Illustration
We illustrate the generalized symbolic execution on a simple
example (see Figure 2). Class Node implements singly-linked
lists; the elds elem and next represent, respectively,
the node's integer value and a reference to the next node.

Figure

3 gives (part of) the corresponding code that was
instrumented for symbolic execution: concrete types were
replaced with \symbolic types" (library classes that we pro-
vide) and concrete operations with method calls that implement
\equivalent" operations on symbolic types. Class
Expression supports manipulation of symbolic integers.
class Node {
Expression elem;
Node next;
boolean _next_is_initialized = false;
boolean _elem_is_initialized = false;
static Vector
static {v.add(null);}
Node _new_Node() {
int
return (Node)v.elementAt(i);
return n;
Node _get_next() {
if(!_next_is_initialized) {
Verify.ignoreIf(!precondition());//e.g. acyclic
return next;
void foo() { .
1: if(_get_elem()._GT(t._get_elem()))
2: _set_next(t._get_next());

Figure

3: Instrumented code
Input structure:
next next
PC: true1
next next
PC: E0>E1 PC:.E.0.<=E1
next
next next next
next
next
next
next
next
next next

Figure

4: Symbolic execution tree (excerpts)
Field reads and updates are replaced by get and set
methods (get methods implement the lazy initialization).
For each eld in the original class declaration, boolean elds
(i.e. next is initialized and elem is initialized) are
added. These elds are set to true by get (set) methods.
Vector v stores the input objects that are created as a result
of lazy initialization. The helper method new Node,
which is called by get node, uses the elements in vector v
to systematically initialize input reference elds, according
to dierent aliasing possibilities.

Figure

4 illustrates the paths that are generated during
the symbolic execution of the code of method foo, for a
given input structure. Each node of the execution tree denotes
a symbolic state. Branching in the tree corresponds to
a nondeterministic choice that is introduced to build a path
condition or to handle aliasing. Edges labelled with numbers
refer to program statements and those without numbers to
lazy initialization steps. The value \?" for an elem eld
indicates that the eld is not initialized and the \cloud" indicates
that the next eld is not initialized; null nodes are
not represented. Structures represent constraints on reference
elds, e.g. the input structure in Figure 4 represents
all (cyclic or acyclic) lists with at least two nodes such that
t points to the second node.
As we will explain later in Section 4.3, method preconditions
can be used during lazy initialization: if the input
structure violates the precondition, the model checker backtracks
(i.e. call to method Verify.ignoreIf in Figure 3).
For example, if we consider the precondition that the input
list should be acyclic, the algorithm does not explore the
transitions marked with an \X" in Figure 4.
3. CASE STUDY: RED-BLACK TREES
We have used our input generation techniques for testing
a variety of programs, including methods of classes in
the java.util package. Most of these programs manipulate
complex data structures. In particular, we illustrate
our techniques on the Java implementation of red-black trees
given in java.util.TreeMap from the standard Java libraries
(version 1.3). Red-black trees [16] are binary search trees
with one extra bit of information per node: its color, which
can be either red or black. By restricting the way nodes are
colored on a path from the root to a leaf, red-black trees
ensure that the tree is balanced, i.e. guarantee that basic
dynamic set operations on a red-black tree take O(log n)
time in the worst case.
A binary search tree is a red-black tree if:
1. Every node is either red or black.
2. The root is black.
3. If a node is red, then both its children are black.
4. Every simple path from the root node to a descendant
leaf contains the same number of black nodes.
All four of these red-black properties are expressible in
Java. We use these four properties together with the basic
properties of binary search trees to dene a repOk method,
i.e. a Java predicate that checks the representation invariant
(or class invariant) of the corresponding data structure. In
this case, repOk checks if the input is a red-black tree. Figure
5 gives part of the java.util.TreeMap declaration and

Figure

6 gives a fragment of code from repOk representing
the third red-black tree property: red nodes have only black
children. The generation of red-black trees is particularly interesting
for our framework, due to their complex structure
(i.e. they have primitive elds, back pointers, etc.
In the next section, we present dierent techniques that
we used to generate test inputs for the implementation of
red-black trees in java.util.TreeMap. We will illustrate
test input generation for several helper methods for the put
and remove methods in class java.util.TreeMap, which are
responsible for adding and deleting the node corresponding
public class TreeMap {
Entry root;
static final boolean
static final boolean
static class Entry implements Map.Entry {
Object
Object value;
Entry left;
Entry right;
Entry parent;
boolean
/* precondition: repOk(root); */
public Object remove(Object key) {.}
public Object add(Object key) {.}

Figure

5: Declaration of java.util.TreeMap
boolean repOk(Entry e) {
.
// RedHasOnlyBlackChildren
while (!workList.isEmpty()) {
Entry current=(Entry)workList.removeFirst();
Entry cl = current.left;
Entry cr = current.right;
if(current.color == RED) {
if(cl != null && cl.color == RED) {
return false;
if(cr != null && cr.color == RED) {
if (cl != null)
if (cr != null)
.
return true;

Figure

to a given key from the tree. We should note that deletion is
the most complex operation among the standard operations
on red-black trees and involves rotations. Together with
the auxiliary methods, addition together with deletion in
java.util.TreeMap are about 300 lines of Java code. The
(implicit) precondition for both put and remove methods
requires the input to satisfy its class invariant (i.e. repOk):
the input must be a red-black tree.
4. TEST INPUT GENERATION
In this section we will illustrate three applications of model
checking to the test input generation of software manipulating
a complex data structure. We will focus on the implementation
of the put and remove methods for red-black trees
in the Java TreeMap library. As a testing criterion we use
source code level branch-coverage since we want to compare
the black-box to the white-box approaches to test input gen-
eration. As mentioned in Section 2.2.3 our framework can
also handle other kinds of testing criteria.
We aim to generate a set of non-isomorphic tests, which
meets the desired coverage criteria. Isomorphism among
tests is dened as isomorphism among graphs where the
heap of a Java program is viewed as an edge-labeled
node identities are permutable, while primitive values are
not [10]. Note that the Java semantics do not allow object
allocation to dictate the exact object identities, which
implies that initializing a test input (at the concrete representation
level by setting eld values or at the abstract
level using a sequence of method invocations) more than
once (say for regression testing) does not generate identical
structures but it generates isomorphic structures.
First we show how a model checker can be used to do the
testing, by executing sequences of method calls in the data
structure's interface. Secondly, we show how we can use our
execution framework to build all (non-isomorphic)
input trees up to a given small size that are to be used for the
(black-box) testing of the method. This is done by symbolically
executing the Java code of the method's precondition
(in this case the code of repOk).
Lastly, we show how our framework can be used for white-box
test input generation and how conservative preconditions
are used during lazy initialization, to stop the analysis
of infeasible paths. We also show how the input constraints
computed by symbolic execution are solved to provide the
inputs for the actual testing.
4.1 Model Checking as Testing
When doing model checking there is a clear distinction
between the system being analyzed and the environment of
the system, i.e. the inputs that the system takes. Whenever
the environment is under-approximated (less behaviors are
considered than are present in the actual environment) during
model checking then model checking becomes a form of
testing. Note that more often than not this is the case during
the model checking of software, since the environment
is usually very large. Considering this connection, one can
therefore use a model checker to generate inputs and analyze
the code on those inputs.
To illustrate this idea we show how one can test the Java
TreeMap library by analyzing all sequences of put and remove
calls on a set with maximally N elements using the JPF
model checker (Figure 7). Note that, for this example, we
are more interested in the coverage of the code, rather than
correctness and hence we only use the model checker's default
properties (uncaught exceptions being the most important
here) as an oracle | in general our approach allows
more general oracles, including method postconditions expressed
as Java predicates.
4.2 Input Generation For Black-box Testing
Our framework can be used to automatically generate
Java data structures from a description of method precon-
public static int
public static TreeMap new TreeMap();
public static Integer[] elems;
static {elems = new Integer[N];
for (int
new
public static void main(String[] args) {
while (true) {
if
else

Figure

7: Model checking as testing
ditions. Note that for sequential code, generalized symbolic
execution explores only paths on non-isomorphic in-
puts. Therefore, we can generate non-isomorphic input structures
that satisfy a precondition, by applying generalized
symbolic execution to the code of the precondition. Once
we have an input structure, we use o-the-shelf constraint
solvers for solving the constraints in the path condition, thus
obtaining the test input. Test inputs can then be used for
black-box testing of the method under test. The drawback
of this approach is that there is no relationship between
the inputs and the code coverage. On the other hand, if one
would be interested in covering the input specication rather
than the code under test, this black-box method achieves full
coverage of the input structures up to a given bound.
In order to test the put and remove methods we automatically
generated all (non-isomorphic) input trees up to
a given small size from the Java description of the method's
precondition (i.e. the structural invariant), thus eliminating
the need to construct the inputs using a sequence of
method calls. Our framework symbolically executes repOk
and it generates the input structures whenever repOk returns
true. We put a limit on the number of generated objects:
whenever the size of the vector that stores the objects created
during lazy initialization (see Section 2) reaches that
limit, the model checker backtracks. As a result, all the input
structures satisfying repOk with size up to the specied
limit are created.
Our approach can be contrasted with a brute force ap-
proach, where one will rst generate all possible trees up
to a given size according to the class denition, and then
would apply repOk to select only valid red-black trees. Our
approach scales better since we generate trees on demand
(with lazy initialization) and we backtrack as soon as a red-black
tree property is violated, thus pruning large portions
of the search space. It is important to note that the actual
structure of repOk is crucial to the eciency of our method.
If repOk would rst evaluate the tree and only at the end
determine whether the tree is valid, our approach would be
equivalent to generating all trees before pruning.
4.3 Input Generation for White-box Testing
Our symbolic execution framework can be used for input
generation during white box testing. To generate inputs
that meet a given testing criterion, our framework is used
to symbolically execute the method under test and to model
check it against properties that encode the testing criterion.
Counterexamples to the properties represent paths that satisfy
the criterion. For every path, our framework also reports
an input structure and a path condition on the primitive input
values, which together dene a set of constraints that
the inputs should satisfy in order to execute that path2.
A particular characteristic of our framework is that it uses
method preconditions during two phases of the input generation
to eliminate infeasible structures:
a conservative precondition, that can deal with partially
initialized structures, is used during lazy initialization
(see Section 4.3.1)
when a counterexample is found the structural constraint
for the path is used as input to a concrete
precondition (the same one used in Section 4.2) to
solve the constraints with only valid inputs (see Section
4.3.1 Conservative Preconditions
We use preconditions in initializing elds (see Figure 3).
In particular, a eld is not initialized to a value that violates
the precondition. Notice that we evaluate a precondition
on a structure that still may have some uninitialized elds,
therefore we require the precondition to be conservative, i.e.
return false only if the initialized elds of the structure
violate a constraint in the precondition.
Consider the analysis of the remove method in the red-black
tree implementations. The method has as precondition
the class invariant of the red-black tree data structure
(i.e. the repOk Java predicate). The conservative version
of the precondition that we used during lazy initialization is
illustrated in Figure 8. Boolean ags left is initialized
and right is initialized were added by our code instrumentation
to keep track of uninitialized input elds (see Section
2.2.4). The code of conservative repOk is identical to
that of repOk, with the exception that the constraints encoded
in repOk are only evaluated on initialized elds.
As an example, assume that there are three input trees as
illustrated in Figure 9 that are created during the analysis
of the remove method (at a lazy initialization step). Round
lled nodes represent entries colored black and empty nodes
represent entries colored red; null nodes are not represented.
As before, a \cloud" denotes an uninitialized eld | intuitively
representing a set of nodes, since it can be lazily
initialized to dierent nodes. For simplicity of presentation,
we omit to represent the key and value elds. Figure 9 also
shows the results of evaluating the conservative repOk on
the tree structures. The rst tree violates the repOk, no matter
what the concrete value of the \cloud" is, since red nodes
cannot have red children. In this case the model checker will
backtrack and it will not consider this structure any further.
The second tree is a concrete structure that satises repOk.
The third tree represents concrete trees that may or may not
satisfy repOk; conservative repOk returns true (or rather
Don't Know), and the analysis continues.
We should note that the lazy initialization of input elds
in our framework is related to materialization of summary
nodes in shape analysis [33], while the conservative preconditions
can be formulated in the context of abstract interpre-
tation. We would like to explore these connections further.
2Our framework also reports the thread scheduling informa-
tion, in the case of multi-threaded code
boolean conservative_repOk(Entry e) {
.
// RedHasOnlyBlackChildren
while (!workList.isEmpty()) {
Entry current=(Entry)workList.removeFirst();
Entry cl = current.left;
Entry cr = current.right;
if (current.color == RED) {
if (current._left_is_initialized &&
cl != null && cl.color == RED) {
return false;
if (current._right_is_initialized &&
cr != null && cr.color == RED) {
return false;
if (current._left_is_initialized &&
cl != null)
if (current._right_is_initialized &&
cr != null)
.
return true;

Figure

8: Predicate conservative repOk
FALSE TRUE TRUE (Don't Know)

Figure

9: Evaluation of conservative repOk on 3
structures
4.3.2 Handling Destructive Updates
The lazy initialization algorithm builds the input structures
on an as needed basis, when they are rst accessed
during symbolic execution. If the code under analysis performs
destructive updates, the structure of the inputs can be
lost. To create test inputs we therefore need to reconstruct
these input structures. As an example, consider the structures
in the leaves of the symbolic execution tree depicted in

Figure

4, which are the result of a destructive update; these
structures no longer contain the information that in the input
structure, there is a link between the rst two nodes. In
order to recover the original input structures, we keep mappings
between objects with uninitialized elds and objects
Solution that
satisfies repOK()
Not a solution!
Symbolic input structure
(Constraint 4 violated.)
satisfying conservative_repOK()

Figure

10: Concretization of symbolic structures
that are created when those elds are initialized; these mappings
are used to reconstruct input structures. Note that
whenever the precondition needs to be evaluated during lazy
initialization, we rst reconstruct the input structures and
then we evaluate the precondition on these reconstructed
input structures.
4.3.3 Solving Constraints
The result of symbolically executing a particular program
path is a heap structure, that encodes constraints on reference
elds, and a path condition, that encodes constraints
on primitive data. These constraints dene the inputs that
will allow the execution of the path. In order to obtain the
actual test inputs, we have to solve these constraints, i.e. we
have to build actual Java data structures that can be used
during testing. In our framework, we solve these constraints
separately for structures and primitive data.
We rst \convert" symbolic structures to concrete structures
that have no uninitialized elds and that also satisfy
the method's precondition. If there are no method pre-
conditions, this amounts to simply setting all the uninitialized
elds to null. Otherwise, the symbolic input structure
(which satises the conservative precondition) is used
as input to the code for the concrete precondition which is
symbolically executed to obtain the concrete structure, in a
way similar to the test input generation method described
in Section 4.2. The constraints in the path condition are
then solved using an o-the-shelf constraint solver.
We should note that not all the concretizations of a symbolic
structure that satises the conservative precondition,
are valid solutions. An example is given in Figure 10.
5. EXPERIMENTS
As mentioned before we measured branch-coverage for the
methods of the TreeMap class and for simplicity we will
only consider here 3 helper methods: deleteEntry (del),
fixAfterDeletetion (xD) and fixAfterInsertion (xI).
The optimal3 branch-coverage that can be achieved for these
methods are 86% (19 out of 22) for deleteEntry, 100% (20
out of 20) for fixAfterDeletion and 88% (14 out of 16) for
fixAfterInsertion. Note that 100% statement coverage
can be obtained for all 3 methods - the uncovered branches
are all for missing else branches where the if option is
always taken.
3The rest of the branches can be shown to be infeasible.
Resources % Coverage
N Time Mem States del xD xI
28
3 2.4 2.3 730 68 5 75
6 Out of Memory

Table

1: Model Checking as Testing
All results were obtained using the JPF model checker
(version 3.1.1) on a 2.2 Ghz dual processor Pentium with 1
Gb of memory running Windows 2000 with Java 1.4.2.
5.1 Model Checking as Testing
The results in Table 1 show the coverage achieved in the
three methods when model checking the code in Figure 7 for
dierent values of N (the number of entries to be added to
the TreeMap). The coverage numbers were gathered using
JPF's facility to calculate branch-coverage on the bytecode
level during execution | a simple transformation was done
to obtain branch-coverage on the source code level. Note
that this technique is also used for the branch-coverage calculations
in the rest of the section. The table also contains
the time taken (in seconds), the memory consumed (in Mb)
and the number of states generated during model checking.
The results indicate that this approach does not scale
well. Until size 4 the results give the appearance of actually
being very good (fast, low memory and reasonable
coverage), but the exponential explosion becomes apparent
at size 5 and size 6 cannot be handled in its entirety. For
fixAfterDeletion, 100% branch-coverage is not achieved;
fixAfterDeletion is called from deleteEntry hence it is
not too surprising that there is a large jump in its coverage
from size 3 to 4.
An advantage of the model checking approach is that it
obtains good path (behavioral) coverage for small input domains
as well as for systems where testing is fundamentally
hard, such as concurrent systems. In the domain considered
here, namely (sequential) programs manipulating complex
data, this technique of testing could be an appropriate rst
pass at nding errors, but to obtain good structural coverage
one needs a more sophisticated approach.
5.2 Black-box

Table

2 shows the results for black-box structural coverage
up to a xed size (N). The input trees were generated
by doing a symbolic execution of the repOk method using
JPF. For each of the input trees all possible node deletions
and one new insertion were then executed (Tests) and the
code coverage measured. We also report the total number
of trees created (Structs) up to a specic size N (in parenthesis
only the number of trees of size N is given) as well
as how many structures where considered (Candidates) by
the lazy initialization of the code within repOk. Since the
memory consumption was minimal (less than 10Mb for the
cases shown) we only report on the time taken to generate
the trees | the time for running the tests were negligible.
Note that since the structures are generated up to a given
size, the results include all the smaller structures as well.
Statistics % Coverage
Structs Candidates Time Tests del xD xI

Table

2: Black-box Structural Tests
Statistics % Coverage
Time Mem Tests del xD xI

Table

3: White-box Tests
After 1 minute all the trees required to achieve optimal
coverage of the code were generated | size 5. Note that
the trees of size N created by analyzing all sequences of
put and remove operations (Section 5.1) are a subset of the
trees of size N allowed by repOk | we believe this is due
to the class invariant (repOk) being more permissive than
the property maintained by sequences of put/remove op-
erations. Indeed (say for performance concerns) methods
may maintain properties that are stronger than the stated
class invariant, thereby disallowing certain structures that
are otherwise valid from being generated during executions
of method sequences.
5.3 White-box
The results from doing a white-box analysis of the methods
of TreeMap to obtain a set of test inputs to achieve
optimal branch-coverage of the three methods is given in

Table

3. We report on the time taken in seconds, memory
usage in Mb, the number of tests run (with the number of
tests generated before removing duplicates in parenthesis)
and the coverage obtained. Although we only mention the
input trees we are considering, each test input consists of an
input tree as well as the node to put/remove.
Note that here we don't parameterize the results with the
size of the trees (as in Table 2), since the goal is to cover all
branches and that is achieved with dierent size trees. We
do however limit the size of the trees that we are looking
for to size 5 and smaller. As to be expected the coverage
obtained is optimal. There are many duplicates amongst
the input trees generated to cover all the 53 branches in the
code | only 11 unique input trees are required. The 11
trees are made up of all trees of size 1, 2, 3 and 4, but only
two trees of size 5 (out of the 8 possible trees).
5.4 Discussion
The lazy initialization of repOk that we use for black-box
test input generation can be compared to the approach taken
by Korat [10]. Korat generates inputs from constraints given
as Java predicates and it uses backtracking (as we also do)
but it monitors executions of repOk on fully initialized inputs
within an a priori given input size. For the example used
here the number of candidate structures the two techniques
consider is very similar. However, if one also introduces integer
values in the structures, our approach considers a lot
fewer structures, since it uses symbolic execution together
with integer constraint solving whereas Korat has to enumerate
the integer elds.
The fact that in the white-box approach only 11 test inputs
are required versus the 84 to obtain the same (optimal)
coverage in the black-box approach illustrates the power of
using a goal-directed white-box approach over a blind black-box
approach to test input generation for obtaining high
coverage. We believe that for more complicated structural
invariants the dierence in test input size for the black and
white box approach would be even more pronounced.
A drawback of our current approach is that we cannot determine
whether code is unreachable when the code contains
cycles | as is the case in the red-black tree examples considered
here. We are considering techniques such as automatic
invariant generation [38] and the use of shape-predicates
and abstraction to address this problem. An inherent draw-back
of symbolic execution is the strength of the decision
procedures used to check for infeasible path conditions. Currently
we can only deal with linear integer constraints, but
we hope to add more powerful decision procedures in the
near future.
We should note that we have experimented with dierent
approaches to representing data structures, e.g. they could
be completely symbolic or represented as partially initialized
Java structures, as in the context of the work presented
here. We used this latter approach because it facilitates the
evaluation of preconditions written as Java predicates.
6. RELATED WORK
6.1 Speci?cation-based Testing
The idea of using constraints to represent inputs dates
back at least three decades [14, 29, 31, 41]; the idea has
been implemented in various tools including EFFIGY [31],
TEGTGEN [32], and INKA [24]. But most of the prior work
has been to solve constraints on primitive data, such as integers
and booleans, and not to solve constraints on complex
structures, which requires very dierent constraint solving
techniques.
Some recent frameworks, most notably TestEra [35] and
Korat [10,34], do support non-isomorphic generation of complex
structures, such as red-black trees. TestEra generates
inputs from constraints given in Alloy, a rst-order declarative
language based on relations. TestEra uses o-the-shelf
SAT solvers to solve constraints. We have already discussed
about Korat in Section 5.4. The Korat algorithm has recently
been included in the AsmL Test Generator [20] to
enable generation of structures. TestEra and Korat focus
on solving structural constraints. They do not directly solve
constraints on primitive data and instead, systematically try
all primitive values within given bounds, which may be in-
ecient. Further, TestEra and Korat have been used for
black-box testing and not in a white-box setting.
An early paper by Goodenough and Gerhart [23] emphasizes
the importance of specication-based testing. Various
projects automate test case generation from specications,
such as Z specications [18], UML statecharts [37], ADL
specications [12], or AsmL specications [25]. These specications
typically do not involve structurally complex inputs
and they do not address object-oriented programs.
Doong and Frankl [19] use algebraic specications to generate
tests (including oracles) for object oriented programs.
Their ASTOOT tool generates sequences of interface events
and checks whether the resulting objects are observationally
equivalent (as specied by the algebraic specication).
Although here we were only interested in generating tests
covering the input structures (black-box) and code (white-
box), using an algebraic specication to create additional
tests and check the functional requirements of the code is a
straight-forward extension.
Gargantini and Heitmeyer [21] use a model checker to
generate tests that violate known properties of a specication
given in the SCR notation. Ammann and Black [3,
4] combine model checking and mutation analysis to generate
test cases from a specication. Rayadurgam et al.
use a structural coverage based approach to generate test
cases from specications given in RSMLe by using a model
checker [26]. Lee et al. [28] dene a framework for using temporal
logic to specify data-ow test coverage.
6.2 Static Analysis
The Three-Valued-Logic Analyzer (TVLA) [33,42] is the
rst static analysis system that can verify preservation of
the list structure in programs that perform list reversals via
destructive updates to the input list. TVLA has been used
to analyze small programs that manipulate doubly linked
lists and circular lists, as well as some sorting programs.
Recently, the TVLA system was extended to also deal with
preconditions on shape-graphs [44]. The pointer assertion
logic engine (PALE) [36] can verify a large class of data
structures that can be represented by a spanning tree back-
bone, with possibly additional pointers. These data structures
include doubly linked lists, trees with parent pointers,
and threaded trees.
While static analysis of program properties is a promising
approach for ensuring program correctness in the long run,
the current static analysis techniques can only verify limited
program properties. For example, none of the above techniques
can verify correctness of implementations of balanced
trees, such as red-black trees. Testing, on the other hand,
is very general and can verify any decidable program property
for realistically large implementations, but for bounded
inputs.
6.3 Software Model Checking
There has been a lot of recent interest in applying model
checking to software [7,8,15,17,22,27,43]. Most of this work
has focused on checking event sequences, specied in temporal
logic or as \API usage rules" in the form of nite state
machines. These approaches oer strong guarantees: if a
program is successfully checked, there is no input/execution
that would lead to an error. However, they typically did not
consider linked data structures or considered them only to
reduce the state space to be explored and not to check the
data structures themselves.
Our work shows how to enable an o-the-shelf model checker
to check for properties of complex structures, taking into account
complex preconditions. Our algorithms can be implemented
in a straightforward fashion to enable other model
checkers that support dynamic structures to check structural
properties too.
Recently two popular software model checkers BLAST
and SLAM, both based on predicate abstraction, were used
to do white-box test input generation [2, 6]. In both cases
the goal is to generate tests that will cover a specic predicate
or a combination of predicates. These techniques do
not focus on generating complex test inputs and they can the class invariant for red-black trees. We would also like to
not handle complex preconditions. thank the reviewers for their detailed comments that allowed
us to greatly improve the paper.
7. CONCLUSION
8.
The main contribution of this work was to show how com-
plex preconditions can be used to allow ecient symbolic
execution of code manipulating complex data to generate
test inputs obtaining high code coverage. In particular we
illustrated how to use a conservative precondition that evaluates
structures (i.e. structures that are not fully
initialized) to eliminate structures that cannot lead to valid
concrete inputs that will achieve the stated coverage. This
conservative precondition can be seen as an abstract version
of the concrete precondition, since it will disallow in- [3]
valid structures, but might accept structures that can be
instantiated to concrete structures that will fail the concrete
precondition. Although we created the conservative
precondition by hand, we would like to investigate how to [4]
generate it directly from the concrete precondition by using
techniques from abstract interpretation. In our experiments
the precondition was the class invariant, but the approach
can handle any precondition expressed as a Java predicate. [5]
We also showed two other approaches to using model
checking and symbolic execution for testing. Firstly, the
most traditional approach from a model checking perspec-
tive, where one simply applies model checking to the system
under test. This approach can obtain high levels of behavioral
coverage, but only for small congurations of data [6]
structures. Secondly, we showed that by symbolically executing
the code for the precondition one can eciently obtain
tests suitable for black-box testing. This second ap- [7]
proach shows the exibility of our lazy initialization approach
to symbolic execution, and it resembles the algorithm
employed by the Korat tool [10] that has been highly
successful in generating test inputs. [8]
We believe that a exible approach to testing complex
software is very important. To this end we think the techniques
covered here can be seen as a continuum in the following
fashion. If the code to be analyzed doesn't have a
full specication, one can use the black-box approach that
only considers the structure of the inputs to generate tests.
[10]
Note that the structure of the inputs must be known and in
our case given as a Java predicate. If a specication does
exist (for example an algebraic specication as used in [19])
then a specication centered approach to test input genera-
tion can be used to augment the above. Note, this requires
the specication to be given in a notation acceptable to a
model checker, again Java in our case. At this point the
black-box approach has been exhausted and one needs to
consider the code (white-box) to generate additional tests.
Although we only considered simple coverage criteria here
to drive the symbolic execution based test input generation,
one can specify any criteria that can be expressed as prop-
erties to the model checker, for example, predicate coverage
[2,6]. Lastly, testing is not sucient in all cases, for example
testing a concurrent program is notoriously incomplete, and
a more powerful technique such as program model checking
can then be used.
[13]

Acknowledgments

[14]
We would like to thank Darko Marinov for insightful discussions
and for sharing with us his Java implementation of


--R

The economic impacts of inadequate infrastructure for software testing.


A specication-based coverage metric to evaluate test sets
Using model checking to generate tests from specications.


Experiments with test case generation and runtime analysis.

Automatically validating temporal safety properties of interfaces.
The SLAM project: Debugging system software via static analysis.
Software Testing Techniques.
Korat: Automated testing based on Java predicates.
International Symposium on Software Testing and Analysis (ISSTA)
Experimental evaluation of verication and validation tools on martian rover software.
Structural specication-based testing: Automated support and experimental evaluation
Model Checking.
A system to generate test data and symbolically execute programs.

Introduction to Algorithms.
Automating formal specication based
Using model
Model checking for programming languages using VeriSoft.
Toward a theory of test data selection.

A temporal logic based theory of test coverage and generation.
An approach to program testing.

Generalized symbolic execution for model checking and testing.
Symbolic execution and program testing.

Automated test data generation for programs with procedures.
TVLA: A system for implementing static analyses.
Testing Using a Solver for Imperative Constraints.
TestEra: A novel framework for automated testing of Java programs.
The pointer assertion logic engine.
Generating tests from UML specications.
Verication of java programs using symbolic execution and invariant generation.
Verication of Time Partitioning in the DEOS Scheduler Kernel.
The Omega test: A fast and practical integer programming algorithm for dependence analysis.
On the automated generation of program test data.
Solving shape-analysis problems in languages with destructive updating
Model Checking Programs
Symbolically computing most-precise abstract operations for shape analysis
--TR
Introduction to algorithms
The ASTOOT approach to testing object-oriented programs
Model checking for programming languages using VeriSoft
Solving shape-analysis problems in languages with destructive updating
Automatic test data generation using constraint solving techniques
A deadlock detection tool for concurrent Java programs
Using model checking to generate tests from requirements specifications
Structural specification-based testing
Model checking
Bandera
Verification of time partitioning in the DEOS scheduler kernel
An Approach to Program Testing
Symbolic execution and program testing
The pointer assertion logic engine
Automatically validating temporal safety properties of interfaces
The S<scp>LAM</scp> project
Software Testing Techniques
Generating finite state machines from abstract state machines
Korat
Model Checking Programs
A Specification-Based Coverage Metric to Evaluate Test Sets
A Temporal Logic Based Theory of Test Coverage and Generation
Automating Formal Specification-Based Testing
TVLA
Toward a theory of test data selection
Using Model Checking to Generate Tests from Specifications
TestEra
Generating Tests from Counterexamples

--CTR
Willem Visser , Corina S. Psreanu , Radek Pelnek, Test input generation for red-black trees using abstraction, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
Automated test generation for engineering applications, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
Nikolai Tillmann , Wolfram Schulte, Parameterized unit tests with unit meister, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
Colin Blundell , Dimitra Giannakopoulou , Corina S. Psreanu, Assume-guarantee testing, ACM SIGSOFT Software Engineering Notes, v.31 n.2, March 2006
Patrice Godefroid, Compositional dynamic test generation, ACM SIGPLAN Notices, v.42 n.1, January 2007
Petri Ihantola, Creating and visualizing test data from programming exercises, Informatics in education, v.6 n.1, p.81-102, January 2007
Carlos Pacheco , Shuvendu K. Lahiri , Michael D. Ernst , Thomas Ball, Feedback-Directed Random Test Generation, Proceedings of the 29th International Conference on Software Engineering, p.75-84, May 20-26, 2007
Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
Rupak Majumdar , Koushik Sen, Hybrid Concolic Testing, Proceedings of the 29th International Conference on Software Engineering, p.416-426, May 20-26, 2007
Nikolai Tillmann , Wolfram Schulte, Parameterized unit tests, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
Michael Emmi , Rupak Majumdar , Koushik Sen, Dynamic test input generation for database applications, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom
Willem Visser , Corina S. Psreanu , Radek Pelnek, Test input generation for java containers using state matching, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
Tao Xie , Jianjun Zhao, A framework and tool supports for generating test inputs of AspectJ programs, Proceedings of the 5th international conference on Aspect-oriented software development, March 20-24, 2006, Bonn, Germany
Sarfraz Khurshid , Yuk Lai Suen, Generalizing symbolic execution to library classes, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
James H. Andrews , Susmita Haldar , Yong Lei , Felix Chun Hang Li, Tool support for randomized unit testing, Proceedings of the 1st international workshop on Random testing, July 20-20, 2006, Portland, Maine
Marat Boshernitsan , Roongko Doong , Alberto Savoia, From daikon to agitator: lessons and challenges in building a commercial tool for developer testing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
Arindam Chakrabarti , Patrice Godefroid, Software partitioning for effective automated unit testing, Proceedings of the 6th ACM & IEEE International conference on Embedded software, October 22-25, 2006, Seoul, Korea
Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, ACM SIGPLAN Notices, v.40 n.6, June 2005
Marcelo d'Amorim , Steven Lauterburg , Darko Marinov, Delta execution for efficient state-space exploration of object-oriented programs, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom
Aysu Betin Can , Tevfik Bultan , Mikael Lindvall , Benjamin Lux , Stefan Topp, Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers, Automated Software Engineering, v.14 n.2, p.129-178, June      2007
Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of data structure properties, ACM SIGPLAN Notices, v.41 n.10, October 2006
Marc Fisher, II , Gregg Rothermel , Darren Brown , Mingming Cao , Curtis Cook , Margaret Burnett, Integrating automated test generation into the WYSIWYT spreadsheet testing methodology, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.2, p.150-194, April 2006
symbolic execution;coverage;testing object-oriented programs;model checking;red-black trees