Partition-Based Regression Verification
Marcel Böhme
School of Computing
National University of Singapore
marcel@comp.nus.edu.sg

Bruno C. d. S. Oliveira
School of Computing
National University of Singapore
oliveira@comp.nus.edu.sg

Abstract—Regression verification (RV) seeks to guarantee theabsence of regression errors in a changed program version.
This paper presents Partition-based Regression Verification (PRV):
an approach to RV based on the gradual exploration of differential input partitions. A differential input partition is a subset ofthe common input space of two program versions that serves as aunit of verification. Instead of proving the absence of regression
for the complete input space at once, PRV verifies differential
partitions in a gradual manner. If the exploration is interrupted,
PRV retains partial verification guarantees at least for the exploreddifferential partitions. This is crucial in practice as verifying thecomplete input space can be prohibitively expensive.
Experiments show that PRV provides a useful alternative tostate-of-the-art regression test generation techniques. During the
exploration, PRV generates test cases which can expose different
behaviour across two program versions. However, while test cases
are generally single points in the common input space, PRV canverify entire partitions and moreover give feedback that allows
programmers to relate a behavioral difference to those syntacticchanges that contribute to this difference.
Keywords-Software Verification, Testing and Analysis

I. I NTRODUCTION
Software verification seeks to guarantee the absence oferrors in a program, but is rather expensive in practice. There
are two main reasons: 1) verification requires specifications,which may be difficult to write and maintain; and 2) theverification process can be very time-consuming.
However, there is some hope for a cheap form of Regression
Verification (RV) [1], [2]. The goal of RV is not to verify thecorrectness of a program ad absolutum but relative to an earlier
version. Thus, RV seeks to guarantee the absence of regression
errors. This more modest goal allows RV to avoid separate
forms of formal specifications. The previous version serves
as sufficient specification for checking whether the changed
version is at least as correct as the previous version.
Yet, in practice, RV for all inputs is very time-consuming.
Godlin and Strichman [1] proposed a decision procedure thattakes two program versions and either proves behavioral equivalence (thus the absence of regression) or provides a witness of
behavioral difference. The authors report that the verificationof non-equivalent versions can take a long time to terminate or
run out of memory. In fact, generally proving the equivalence
between two programs is an undecidable problem. While thetermination of RV provides strong regression guarantees for
all inputs, the interruption of the verification procedure (dueto time or memory constraints) yields no guarantees at all.

978-1-4673-3076-3/13/$31.00 c 2013 IEEE

5HJUHVVLRQ9HULILFDWLRQ

Abhik Roychoudhury
School of Computing
National University of Singapore
abhik@comp.nus.edu.sg

3DUWLWLRQEDVHG
5HJUHVVLRQ9HULILFDWLRQ

5HJUHVVLRQ7HVWLQJ

8QYHULILHG,QSXW6SDFH
9HULILHG,QSXW6SDFH

Fig. 1.

PRV versus Regression Verification and Regression TestingThis paper presents Partition-based Regression Verification(PRV), a gradual approach to RV based on the explorationof differential partitions. A differential partition is a subsetof the common input space of two program versions thatserves as unit of verification. Instead of verifying the entire
input space at once, PRV allows gradually verifying suchpartitions one-by-one. As illustrated in Figure 1, PRV shares
the advantages of both, Regression Testing (RT) and RV.
Like RV, if all differential partitions are shown equivalent, thenPRV guarantees the absence of regression errors for all inputs.
More importantly, PRV allows a form of partial verification:
if the verification procedure is interrupted, PRV guarantees
the absence of regression errors for the explored partitions
that are shown equivalent. Thus, like RT, PRV allows thegradual checking for regression. However, while RT provides
verification guarantees only for the concrete, executed sample
inputs, PRV seeks to guarantee the absence of regression
for entire input partitions. In practice, this partial verification
approach is crucial, as verifying the complete input space canbe infeasible due to time or other resource constraints.
Technically, differential partitions are computed using aform of symbolic execution [3] and require deterministic
program execution. In contrast to other input partitioning
techniques [4]–[8], differential partitioning accounts for the
inputs of two programs. A differential partition is characterized
by a symbolic condition that defines a range (or subset) ofvalid input for that partition. Input is grouped according towhether it reaches the same syntactic changes and whether
it propagates the same differential state to the output. If an
input computes the same output in both versions, the respective
partition is said to be equivalence-revealing. In such case, bothversions are soundly guaranteed to compute the same output
for all input satisfying the symbolic condition. Otherwise, therespective partition is said to be difference-revealing.

300

ICSE 2013, San Francisco, USA

⌥

1
2
3
4
5
6
7

⌃

8

input(i);a = 0; o = 0;i = i; //i=i+1
if(i>0)a++;if(a>0)o=i;output(o);(a) Programs P and P’

Fig. 2.

⌅

P
P’

⇧

PRV

Input
i0
i>0
i+10
i+1>0
i<0
i=0
i>0

Outputo=0o=io0 = 0o0 = i + 1
o = o0o = 0 ^ o0 = i + 1
o = i ^ o0 = i + 1

D ([HFXWH7HVW&DVH

E &RPSXWH'LIIHUHQWLDO3DUWLWLRQF *HQHUDWH1H[W7HVW&DVH

G &RQWLQXRXV([SORUDWLRQ

8QH[SORUHG3DUWLWLRQ:LWQHVVLQJ7HVW&DVH(TXLYDOHQFH5HYHDOLQJ3DUWLWLRQ'LIIHUHQFH5HYHDOLQJ3DUWLWLRQ(b) Differential Partitions

Running Example (Incomplete Bugfix)

Figure 2 illustrates differential partitions in a concrete
example. Program P computes output o based on the valuesof input i and is changed to P 0 by substituting line 3 with thecommented code. Figure 2.b shows the symbolic output thatis computed based on the evaluation of the input variables forboth programs. The bottom three rows depict one equivalencerevealing and two difference-revealing input partitions. Notethat the analysis of only a single version is insufficient toexpose all interesting subsets of input. In particular, a test suiteT{i = 1, i = 1} covers all paths in both programs andeven reveals a difference. However, input i = 0 is a missing
test case that could represent a regression error. Intuitively,
it is interesting because the branch in line 4 is evaluated indifferent directions in both versions. PRV explores a distinct,
difference-revealing partition for this input.
PRV provides an alternative to regression test generation
techniques [9]–[12]. Upon allowing the continued explorationeven of difference-revealing partitions, the developer may(in)formally verify such partitions. The test cases generated foreach difference-revealing partition can be checked against thedeveloper’s expectation. The program slice, used to computethe partition, can be inspected to determine the changed statements contributing to the difference. The symbolic conditions
and summaries (cf. Fig. 2.b) can be further analyzed by tools.
Our initial experience with PRV is very encouraging. For thestudied subjects, PRV efficiently exposes regression errors thatare not detected by the considered test generation methods.
In summary the main contributions of this paper are:
• A gradual approach to regression verification that continuously verifies the input space of a program against
another version of that program to find regression errors.
If the verification procedure is interrupted, PRV guarantees the absence of regression errors for the exploredinput space that has been shown equivalence-revealing.
• A differential partitioning technique, based on symbolic
execution, that soundly partitions the input of two versions. The partitioning technique symbolically groups
input of the two programs, and creates partitions which
either guarantee behavioral equivalence, or expose differences for a certain subset of inputs.
• An alternative to regression test generation. The approach
can be used to generate test cases for partitions where
differences are found. As illustrated by our experimental
evaluation, finding such test cases is competitive withstate-of-the-art regression test generation techniques.
• The implementation and experimental evaluation of PRV.

Fig. 3.

Exploration of Differential Partitions

II. PARTITION - BASED R EGRESSION V ERIFICATIONPRV takes two successive program versions and continuously verifies differential partitions (Def. 1). The gradualregression verification can be interrupted at any time. In thiscase, the regression guarantees are retained for the verified
input space. For every partition, PRV generates a concrete
sample input that is added to regression test suite T . The
programmer can check difference-revealing test cases in T
for regression errors and relate an output difference to theset of syntactic changes that contribute to that difference. The
intuition of partition-based regression verification is presented
in Figure 3, while the detailed procedure is outlined in Algorithm 1. Later, in Theorem 2, we will claim the exhaustivenessof this exploration algorithm.
Definition 1 (Differential Partition)
A differential partition dP,P 0 is obtained by partitioning of
the common input space of two program versions P , P 0 .
Inputs in any differential partition dP,P 0 have the following
property: either all inputs in dP,P 0 produce the same output
in P and P 0 (an equivalence-revealing partition), or all inputs
in dP,P 0 produce different outputs in P and P 0 (a differencerevealing partition).
The exploration starts with a random test case in the queue.
Depicted as black dot in Figure 3.a) this random test case t istaken from the queue and executed upon both versions. Test
case t is a point in the common input space1 of both versions, representing concrete knowledge about the differential
behavior. In Figure 3.b), input is grouped into a differential
partition that yields the same differential behavior as t. This
input exercises all those statement instances that are “relevant”
to the reachability and propagation of the syntactic programchanges exercised by t. Hence, in Algorithm 2 the symbolic
condition is computed as a conjunction of the pertinent branch
conditions. Later, in Theorem 1, we will claim the soundnessof this generalization from a test case to a differential partition.
1 The derivation of the common input space for versions with different input
spaces is discussed in [9], e.g., the new version has one more input variable.

301

Algorithm 2 - Procedure computeDPartition
Algorithm 1 Partition-based Regression Verification
Input: Input t, Versions P and P 0 , Changes C and C 0
Input: Versions P and P 0 , Changes C and C 0
1: let trace ⇡execute(t, P )1: let queue;
2: let trace ⇡ 0
execute(t, P 0 )2: let T;
3: let conditionf alse3: let V;
4: if not exist an instance of c0 2 C 0 in ⇡ 0 then
4: add randomInput() to queueV005:
let condition
5: while queue 6= ; do
c0 2C 0 reach(c , ⇡ )6: else6:
let tchooseN extT estcase(queue)
7:
let oi be the instance of output o in ⇡7:
let condition
computeDP artition(t, P, P 0 , C, C 0 )8:
let o0i be the instance of output o in ⇡ 0
8:call generateAdjacentT estcases(condition, queue)9:
if value(oi ) = value(o0i ) then9:
add t to T
10:
let condition
prop(o, ⇡, ⇡ 0 , C, C 0 )10:
add condition to V
11:else
11: end while12:
let condition
dif f (o, ⇡, ⇡ 0 , C, C 0 )Output: Verified Input Space V , Regression Test Suite T
13:
end if
14: end if
As depicted in Figure 3.c), the next test case is executed
Output: Condition condition
outside of the explored input space. To generate such “adjacent” test cases, the constituent branch conditions are negated
one-by-one (cf. Alg. 4), similar to other path exploration techInput that yields different output is difference-revealing.
niques. This yields a number of intermediate constraints. If a If t yields different output in both program versions, thenconstraint solver finds a satisfying witness to one of these con- PRV employs the difference condition (Def. 5) to group input
straints, then it is added to the queue waiting to be executed. that computes different output for the same “reason”. These
As depicted in Figure 3.d), after the execution of the next reasons are defined upon the exercised dynamic and static
test case from the queue, again, the corresponding differential program dependencies, as enunciated in the following.
partition is computed. This procedure repeats until all differential partitions are explored or some (time) budget is exhausted. B. Computing Reachability Conditions
A search strategy would assign some distance or fitness toIntuitively, an input t does not execute a changed statement ceach constraint and decide the order in which the partitions
because the conditions of the branch instances si upon whichcorresponding to intermediate constraints are explored. This isc statically control-depends are evaluated in the direction that
implemented in the procedure chooseNextTestcase (not listed).
does not favor the execution of c.
In particular, PRV takes from the queue in the order they arrive⌥⌅
but prioritizes test cases that promise 1) different output, 2) the1
input(i,j);
propagation of already exercised changes and 3) the execution2
a = 0; b = 0;of another set of changes, in that order. Finally, every executed3
if(i>0)4
a=1;
test case is added to the regression test suite T . Each test case5
for(c=0; c < j; c++)is a witness of one differential partition. The set of explored6
b += c;differential partitions V represents the verified input space.
7
if(j>0)8⌃

A. Computing Differential Partitions

9

The computation of the differential partition for a given test
case is presented in Algorithm 2. It implements the functionality of procedure computeDPartition called in Algorithm 1
and requires determinism - for every execution of the same
input on the same program the same output is computed. Also,
the deletion of variable assignments (e.g., x=x++) in P isrepresented by dummy-statements (e.g, x=x) in P 0 (cf. [13]).
Upon execution of the test case t on both programs, P and
P 0 , the symbolic condition is computed. Input that does not
exercise a syntactic change or that does not propagate thedifferential state to the output is equivalence-revealing. If t
does not exercise a changed statement, then PRV employs thereachability condition (Def. 3) to group input that does not
execute a change for the same “reason”. If t exercises at least
one changed statement but yields the same output in both versions, then PRV employs the propagation condition (Def. 4).

Fig. 4.

if(a>0)//change c⇧

Intuition of Reachability Condition

An example is shown in Figure 4. Input (0, 1) does not
execute the changed statement in line 9. Why? Because thebranch in line 8 is not evaluated to true. This is because thecondition in line 7 is evaluated to true and the condition inline 3 to false. The remainder of this section explains thecomputation of the reachability condition based on the relevantslice of the branch in line 8.
Definition 2 (Relevant Slice [14], [15])302

Given an execution trace ⇡ and a statement instance si in ⇡,the relevant slice of si in ⇡ contains all statement instances ri
in ⇡ that are in the transitive closure of dynamic data, controland potential dependence of si .

A statement instance si potentially depends [14] on conditional
statement instance ri in path ⇡ iff. there exists a variable v
used in si such that (1) v is not defined between ri and si in⇡ but there exists another path from ri to si along which
v is defined, and (2) evaluating ri differently may cause thisuntraversed path to be executed.
Note that relevant slices have a desirable property: If two
inputs t0 and t1 exercise the same relevant slice computed
w.r.t. a statement instance si , then the variables used in si
have the same symbolic values for t0 and t1 [7]. Relevantslices are used to define the reachability, propagation, anddifference conditions. The property of relevant slices is utilized
to prove Theorem 1, establishing that these conditions indeed
characterize differential partitions as defined in Definition 1.
Definition 3 (Reachability Condition)
The reachability condition, reach(c, ⇡), computed over the
trace ⇡ w.r.t. statement c is the path condition computed overthe union of the relevant slices of all instances si in ⇡ of every
statement s that c transitively, statically control-depends on.
If an input t0 does not exercise statement c, then every
input t1 satisfying reach(c, ⇡(t0 , P )) does not exercise c. A
path condition is a quantifier free first order logic formula on
program inputs. Any test input satisfying the path condition ofa path ⇡ is guaranteed to also exercise all statement instancesin path ⇡. The negation of a constituent branch condition in thereachability condition computed w.r.t. statement c may change
the reachability of c.
C. Computing Propagation Conditions
Intuitively, an input t does not propagate the semantic
effect of the exercised changes to the output because certain
statement instances Ni upon which the output dynamicallydepends carry the same values in both versions. On a highlevel, Ni represents the point where the differential program
states converge. Any attempt of negating a branch beyond thatpoint to propagate a difference in program state is futile.
















IDOVH



R





D



IDOVH
D 2OG9HUVLRQ3

Fig. 5.

IDOVH



R





D



IDOVHE 1HZ9HUVLRQ3

Intuition of Propagation Condition

Figure 5 shows the dynamic dependency graphs augmented
by concrete values and computed for the execution of input( 1) upon the version pairs in Figure 2. The dashed arrows
indicate potential dependence while the concrete arrows indicate either dynamic data- or control-dependence. Each nodeis labeled with the line number of the statement instance it

represents. The values for the instance of line 3 are different
in both versions. That is, the program state is “infected” after
the execution of the change. However, the value of the output
in line 8 is the same for both versions. Why?
The semantic effect of the change in line 3 is not propagatedto the output in line 8 for the execution of ( 1) on P and P 0
because the branch in line 4 is evaluated in the same direction
in both versions even though it dynamically depends on thestatement in line 3, which carries different values in bothversions. In the remainder of this section, we explain how
the instance of line 4 is added to the convergence set Ni anddefine the propagation condition based on Ni .
As shown in Algorithm 3, both dynamic dependency graphs(DDGs) are computed over the traces ⇡ and ⇡ 0 for the
execution of input t on both versions P and P 0 . The DDGs areaugmented by potential dependencies and the concrete values
for the variables used in every node. Output instances oi in ⇡and o0i in ⇡ 0 are aligned and passed into procedure P ROPA LIGN
to compute Ni recursively.
Algorithm 3 Computing Differential State Convergence Ni
Input: Execution Traces ⇡ and ⇡ 0 , Output Statement o
1: aDDG
augmentedDDG(⇡)
2: aDDG0
augmentedDDG(⇡ 0 )
0
3: (oi , oi )alignableOutput(aDDG, aDDG0 , o)
4: Ni;
5: if isChanged(o0i ) then add (oi , o0i ) to Ni
6: else call P ROPA LIGN (oi , o0i )7: procedure P ROPA LIGN (si , s0i )8:Ri
si .getDependsOn()
9:Ri0
s0i .getDependsOn()
10:
for all ri0 2 Ri0 do
11:
if ¬isChanged(ri0 ) ^ 9ri 2 Ri . align(ri , ri0 ) ^(value(ri ) = value(ri0 )) then12:call P ROPA LIGN(ri , ri0 )
13:
else
14:
add (si , s0i ) to Ni and return15:
end if16:
end for17: end procedure
Output: Statement instances Ni
Assuming that instances si and s0i can be aligned, the tuple(si , s0i ) is added to the set Ni if 1) not all of the “subsequent”
instances ri0 can be aligned, 2) the values of the variables usedin ri and ri0 are different, or 3) ri0 is a changed statement. Thisis represented by the intuitively named predicates in line 10.
Note, we do not assume that both DDGs can be aligned
completely, which would be rather difficult indeed due tothe different number of instances every statement can have inboth executions. Instead, the alignment begins from the output
statement instances (e.g., return), which we assume to bealignable, and follow the dependence edges recursively. The
instance at which alignment fails is added to Ni . In Figure 5,
the instances in line 4 are added to Ni because they depend on
the changed statement in line 3 that also has different values.

303

Definition 4 (Propagation Condition)
Let statements C in program P be changed to C yielding
P 0 . Given traces ⇡ and ⇡ 0 for the execution of input t on P
and P 0 and Algorithm 3 computes Ni for ⇡ and ⇡ 0 and program output statement o, the propagation condition is defineddef
as prop(o, ⇡, ⇡ 0 , C, C 0 ) = 8(ni , n0i ) V
2 Ni .rsc(ni , ⇡) ^
0
0
0
rsc(n
,
⇡
)
^
value(n)=
value(n)^
iiic2C reach(c, ⇡) ^V00reach(c
,
⇡
).
0
0
c 2C
0

Every input satisfying the same propagation condition does
not propagate the effects of the exercised changes for the same
reason. Hence, Definition 4 is a conjunction of five conditions.
The necessary conditions 1) and 2) leverage the property of
relevant slices. Note, rsc(ni , ⇡) is the path condition computed
over the relevant slice of statement instance ni in trace⇡. Every input exercising the same relevant slice w.r.t. ni ,compute the same symbolic value for ni . The negation of aconstituent branch condition may change the computation ofni and thus enable propagation. The necessary condition 3)
captures that the symbolic values for the alignable instancesin Ni are the same. The negation of such an equivalence
condition may enable propagation. The necessary condition
4) and 5) captures that those changes (not) exercised by thetest case t are also (not) exercised by other input satisfying
the same propagation condition. The negation of a constituent
branch condition may enable the reachability of other changes.
D. Computing Difference Conditions
Intuitively, input t computes different output because it exercises a certain set of statement instances in P that contributeto computing the symbolic output of P and another set ofstatement instances in P 0 that contribute to computing thesymbolic output of P 0 .
Definition 5 (Difference Condition)
Let statements C be changed to C 0 . Given instances oi of
output statement o in trace ⇡ and o0i of o in trace ⇡ 0 , thedefdifference condition is defined as dif f (o, ⇡, ⇡ 0 , C, C 0 ) =
0
0
0
rsc(o
V i , ⇡) ^ rsc(oi ,V⇡ ) ^ value(o0 i ) 0 6= value(oi ) ^c2C reach(c, ⇡) ^c0 2C 0 reach(c , ⇡ ).

Every input satisfying the same difference condition propagates the semantic effect of the exercised changes for the same
reason. To achieve this property, Definition 5 is a conjunction of five necessary conditions. The necessary conditions
1) and 2) leverage the property of relevant slices. Every
input exercising the same relevant slice w.r.t. oi , compute thesame symbolic value for oi . The negation of a constituent
branch condition may change the computation of oi and thus
disable propagation. The necessary condition 3) captures thatthe symbolic output values are different in both versions.
The negation of this condition may disable propagation. The
necessary conditions 4) and 5) capture that those changes (not)in ⇡ or ⇡ 0 are also (not) exercised by other input satisfying
the same difference condition. The negation of a constituent
branch condition may enable the reachability of other changes.

A set of changed statements Ct semantically interferes forthe execution of input t on both program versions, if t yields
different output in P and P 0 and every c 2 Ct contributes tocomputing the output. Thione et al. [16] approximate semanticinterference based on static data- and control-dependence. It
can be used to understand the origin of regression.
Interestingly, every changed statement in the relevant sliceof o0i contributes in computing o0i and therefore semanticallyinterferes. This allows the developer to inspect the set ofchanges responsible for an observed semantic difference.
E. Generating Adjacent Test Cases
Algorithm 4 generates “adjacent” test cases from the provided symbolic condition and adds those to the queue. It
implements generateAdjacentTestcases called in Algorithm 1.
Algorithm 4 - GENERATE A DJACENT T ESTCASES
Input: Condition cond, Queue queue0
1: let cond = ( 00 ^. . .^ m)^( 0 ^. . .^ n )^( 0 ^. . .^ k )2: for all i in [ 0 , .., k ] do
0
3:constr( 00 ^ . . . ^ m) ^ ( 0 ^ . . . ^ n) ^ ¬ i+
4:if exists t that satisfies constr then5:
add t+ to queue
6:
end if
7: end for
8: let ('0 ^ . . . ^ 'n )reorder( 0 ^ . . . ^ n )9: for all i from n to 0 do
010:
constr( 00 ^ . . . ^ m) ^ ('0 ^ . . . ^ 'i 1 ^ ¬'i )+11:
if exists t that satisfies constr then12:
add t+ to queue13:
end if
14: end for0
15: let ('00 ^ . . . ^ '0m )reorder( 00 ^ . . . ^ m)
16: for all i from m to 0 do
17:
constr'00 ^ . . . ^ '0i 1 ^ ¬'0i+
18:
if exists t that satisfies constr then19:
add t+ to queue20:
end if
21: end for
Output: Queue queue
The symbolic condition is composed of branch conditions
0( 00 ^ . . . ^ m) in P 0 , branch conditions ( 0 ^ . . . ^ n )in P , and equivalence conditions of the form value(si ) =value(s0i ) or value(si ) 6= value(s0i ) (cf. line 1). First, theconstituent equivalence conditions 0 to k are negated oneby-one (lines 2-7). If there exists a solution to the computed constraint, it is added to the queue. Second, if somebranch conditions are removed from a path condition, theremaining branch conditions have to be reordered before
negation (lines 8-9). Otherwise, the exploration algorithm
ceases to be exhaustive (cf. [7]). Hence, the branch conditions( 0 ^ . . . ^ m ) in P are reordered as follows: If a branch
instance b is in the relevant slice of branch instance bk ,then the branch condition of b is placed before the branch304condition of bk . Otherwise, the branch condition of b isplaced after the branch condition of bk . The reordered branch
conditions in P are negated one-by-one and conjoined with0
( 00 ^ . . . ^ m) in P 0 (line 10-15). If there exists a solution to
the computed constraint, it is added to the queue. Lastly, thebranch conditions in P 0 are reordered and negated one-by-one(lines 16-23). Again, if there exists a solution to the computed
constraint, it is added to the queue.

Every version of the same subject uses the same test driverto construct necessary input objects, strings, or arrays fromthe input integers that come as solution to a first-order logic
formula from the Z3-constraint solver [25]. The subject programs are analyzed on a desktop computer with an Intel 3GHz
quad-core processor and 4GB of memory.

F. Theorems

The subjects summarized in Figure 6 are chosen according
to two criteria: 1) they represent a variety of evolving programsand 2) are discussed in related work (which allows thecomparison with our own experimental results). There are 83
versions of programs ranging from 20 to almost 5000 lines
of code (LoC). Some versions are derived by seeding faults,
called mutants, of the original versions. Some are real versions
that were committed to a version control system.

In the following, we postulate the soundness of Algorithm 2that computes the differential partition for a given test case andthe exhaustiveness of Algorithm 1 that explores differential
partitions. For the lack of space, the detailed proof has been
moved to the corresponding technical report [17]. In practice,
the absence of regression errors can be guaranteed for all
inputs to the same extent as symbolic execution can guarantee
the absence of program errors (see e.g., [18]). Specifically, we
assume deterministic program execution.
Theorem 1 (Sound Generalization)

B. Subject Programs

Subject Reference
Classes Functions LoC Versions
Min [26]
1
1
20
5
Tcas [1], [13], [27], [28]
1
8
166
21
Replace [12], [27]
1
21
564
33
Siena [12]
6
107
1529
7+11
Apache CLI
22
183
4966
6
Total
30
320
7245
83

Given statements C in program P are changed to C 0 yielding
P 0 , every input satisfying the condition computed by Algorithm 2 for input t is in the same differential partition as t.
Informally, the differential behavior of a point in the common input space is soundly generalized to the set of points inthe same differential partition. In particular, let Algorithm 2compute the symbolic condition
for a test case t. If t
is equivalence-revealing, then every input satisfying
isequivalence-revealing. Similarly, if t is difference-revealing,
then every input satisfying is difference-revealing.
Theorem 2 (Exhaustive Exploration)
If there exists an input t0 that computes different values forthe output o in versions P and P 0 and Algorithm 1 terminateswith regression test suite T , then there exists a test case t 2 T
so that t0 satisfies dif f (o, ⇡(t, P ), ⇡(t, P 0 ), C, C 0 ).
Informally, if the verification procedure terminates then all
differential partitions have been explored. The respective proof
leverages the exhaustiveness of the exploration based on
relevant slices as shown in [7].
III. E MPIRICAL S TUDY

Fig. 6.

We compare the empirical results of the references discussing regression verification [1] and regression test generation [12], [13], [27], [28]. Note, there are no empirical results
available for the regression test generation techniques [10],[11], [29] and differential symbolic execution [30].
Min [26] is a short function introduced to discuss the
problem of equivalent mutants. An equivalent mutant is a
simple syntactic change to a program that yields no semantic
difference. Tcas is the traffic collision avoidance system. This
well-studied program is available in the SIR [31] with several
versions that contain seeded faults. We chose the first 20
changed versions. Replace performs pattern matching andsubstitution and is available in the SIR with 32 versions that
contain seeded faults. Siena is an event notification architecture. Note, there are 7 versions available in the SIR and forevery version there exist between one and four faulty versions(in total 11 mutants).
Revision Submission Developer’s Submission Comment
129800 15.08.2002 bug. no 11680 resolved
129803 18.08.2002 bug #11457: implemented fix [..]
129843 14.11.2002 added fix for Rob’s problem [..]
129849 19.11.2002 some bug fixes submitted by Rob [..]
538031 15.05.2007 Applying Brian Egge’s fix from CLI-13
667565 13.06.2008 Restored CLI 1.0 behavior (CLI-137)

Our experiments evaluate the relative efficiency of PRV anddiscuss practicability based on our experience. The experiments do not prove the scalability of PRV. In fact, PRV suffersfrom the same limitations as symbolic execution. Similarly,
it can benefit from relevant optimizations such as domain
reduction [19], [20], parallelization [21], and better searchstrategies [22], [23].

Fig. 7.

A. Setup and Infrastructure
PRV has been implemented into our dynamic backward
slicing tool JSlice [24]. The differential partitions are exploredin a breadth-first manner starting from the same initial input
within the time bound of five minutes, unless stated otherwise.

Subject Programs

Apache CLI Revisions (http://commons.apache.org/cli/)

Apache CLI is an open source command line interpreter.
We retrieved the six revisions from the version control system(branches/cli-1.x/src) that are presented in Figure 7 along withthe submission date and comments and the unique identifiers.

305

All programs are tested as whole programs, except for
Apache CLI. In this case, the the command line component
was tested for regression. The first three programs all have amain method. For Siena, encode and decode in the class
SENP serve as main methods. For Apache CLI, addOption
and getOptionValue in the class CommandLine serve as
testing hooks.

TABLE IF IRST W ITNESS OF S EMANTIC D IFFERENCE
P, P 0
PRV

Average Time in sec
Min (4 Mutants)
0.4
0.3 (-25%)
0.3 (-25%)
Tcas (20 Mutants)
5.6
20.9 (+273%) 20.7 (+270%)
Replace (32 Mutants)
22.8 130.5 (+472%) 60.1 (+164%)
Siena (11 Mutants)
30.7
66.2 (+116%) 40.4 (+32%)
Siena (7 Versions)
14.0
18.3 (+31%)
12.7 (-9%)
Apache CLI (6 Versions)57.8
38.9 (-33%)
45.1 (-22%)
Mutation Score - fraction of versions shown semantically different
Min (4 Mutants)
0.75
0.50 (-33%)
0.50 (-33%)
Tcas (20 Mutants)
1.00
0.56 (-44%)
0.56 (-44%)
Replace (32 Mutants)
0.76
0.56 (-26%)
0.63 (-17%)
Siena (11 Mutants)
0.82
0.73 (-11%)0.73 (-11%)
Siena (7 Versions)
0.67
0.67 (±0%)
0.67 (±0%)
Apache CLI (6 Versions)
1.00
1.00 (±0%)
1.00 (±0%)

C. Research Questions
RQ1: How efficiently does PRV find the first input that exposessemantic difference?
Empirical studies in the discussed related work are concernedwith finding the first difference-revealing input as witness ofsemantic difference. We compare the efficiency of PRV to theefficiency reported in related work.
RQ2: How efficiently does PRV find the first input that exposes
software regression?
Not every difference-revealing input exposes software regression. In fact, after syntactic changes to the program, semanticchanges may be anticipated in the form of progression. For
instance, when a buggy program is fixed input failing in the
buggy version is supposed to pass in the fixed version. To
classify a semantic change as regression, we have to definecorrectness. As often in reality, we assume the absence offormal specifications. In this scenario, the developer checks
the generated difference-revealing test cases informally against
her expectation. If she observes regression, the developer canrelate the regression-revealing test cases to the changes thatsemantically interfere.
RQ3: How practical is PRV in an example usage scenario?
The subject Apache CLI shall be used to evaluate PRV in apractical usage scenario. PRV generates difference-revealing
test cases within the bound of 20 minutes for every version
pair. We classify the generated test cases (e.g. regressionrevealing) and compare the (informal) measure of regression
and progression to the submission comments in Figure 7.
IV. R ESULTS AND A NALYSIS
RQ1: Efficiency - Semantic Difference
We measure two aspects when searching for the firstdifference-revealing input as shown in Table I. The first sevenrows show the average time to find a difference-revealing input
per subject. If for a version pair none of the approaches finds
a difference-revealing test case within five minutes, then it
does not contribute to the calculation of the average time. The
mutation score depicts the fraction of versions for which a
difference-revealing input can be found within five minutes.
To gather results for the symbolic execution of the changed
version P 0 , we implemented a DART-like [6] and eXpresslike [12] path-exploration technique (Columns 3-4) into JSlice.
The DART-like technique explores all paths in P 0 while the
eXpress-like technique prunes all paths that do not exercise achanged statement in P 0 . The results for the exploration of thedifferential behavior of both versions, P and P 0 , are gatheredusing PRV (Column 2).

only P 0
DART-like
eXpress-likeAnswer to RQ1. For the analyzed subjects, PRV generates
a difference-revealing test case on average for 21% moreversion pairs in 41% less time, than the eXpress-like approachthat analyzes only the changed version P 0 . For the subtle,
seeded faults PRV can find a difference-revealing test casemore efficiently. In particular, Tcas is fully analyzed within
the time bound by all approaches but only PRV can find adifference-revealing test case for every mutant supporting the
motivation illustrated in Figure 2. In general, PRV’s relative
efficiency is better for the first four subjects containing subtle,
seeded faults. This efficiency reduces as the changes become
more complex in the latter two subjects. This can be attributed
to the increased number of changed statements correlating withan increased probability to reveal a difference (for random
input). However, not every difference-revealing test case isalso regression-revealing as analyzed in RQ2.
Compared to DART, our eXpress-like implementation has
a similar relative efficiency than eXpress in [28] and [12].
The authors compare full path exploration (Pex) to pruning
paths that do not execute a changed statement (Pex-eXpress).
For Siena, Replace, and the chosen mutants of Tcas, theauthors report an improvement in terms of time of 29%, 57%,
and 13%, respectively. For these subjects, we see a similar
improvement of 37%, 54%, and 16% of the eXpress-likeapproach over the DART-like approach, respectively.
Mutation Score
Tcas
ReplaceFig. 8.

Matrix [13]62.7%-SHOM [27]62%72%

PRV [this]
100%
76%

PRV mutation scores vs SHOM and Matrix

Santelices et al. [13] and Harman et al. [27] report the
mutation score for the test generation tools Matrix and SHOM,
respectively. Note that many of the subjects used by these authors and us are different. However, Tcas was used to evaluate
Matrix and SHOM, while Replace was also used to evaluate
SHOM. As shown in Figure 8, PRV compares favourably
for the commonly evaluated subjects, Tcas and Replace. The
last row shows the average mutation score for the subjects
evaluated in the respective references. In contrast to these306

search-based techniques, PRV avoids searching for differencerevealing test cases within the already explored input space.
This may help explaining the observed improvements.
Godlin et al. [1] evaluate the implementation of regression
verification using randomly generated programs and Tcas. It
takes many hours or the system runs out of memory whenanalyzing non-equivalent programs. Offutt et al. [26] discuss
the problem of equivalent mutants using subject Min. PRV
guarantees equivalence for Mutant 3 and provides a witness
for the other non-equivalent mutants in less than a second.

TABLE IIF IRST W ITNESS OF S OFTWARE R EGRESSION
P, P 0
PRV

Average Time in sec
Min (4 Mutants)
0.4
0.3 (-25%)
0.4 (-25%)
Tcas (20 Mutants)
5.6
20.9 (+273%)
20.7 (+270%)
Replace (32 Mutants)
22.8 130.5 (+472%)
60.1 (+164%)
Siena (11 Faulty Versions)17.6
50.4 (+186%)
44.1 (+151%)
Apache CLI (6 Versions) 141.3 259.6 (+84%)
263.9 (+87%)
Mutation Score - fraction of versions exposed as regression
Min (4 Mutants)
0.75
0.50 (-33%)
0.50 (-33%)
Tcas (20 Mutants)
1.00
0.56 (-44%)
0.56 (-44%)
Replace (32 Mutants)
0.76
0.56 (-26%)
0.63 (-17%)
Siena (11 Faulty Versions)0.55
0.45 (-17%)0.45 (-17%)
Apache CLI (6 Versions)0.40
0.20 (-50%)
0.20 (-50%)

RQ2: Efficiency - Software Regression

Y([SHFWHG

$FWXD
O&KD
Q

([SHFWHG
Y

Y

Y

YQ

YB0XW

JH$FWXDO&KDQJH

D 6LHQD

Fig. 9.

E $SDFKH&/,How to Measure Regression?

How do we measure regression? For Siena, we simulate
an incomplete bug fix [32] from one version to the next.
An example is shown in Figure 9.a). The programmer fixes
Siena.v0 which is expected to behave like Siena.v1. Instead,he introduces another bug yielding Siena.v1 Mut1 – a versionof Siena.v1 that also contains seeded faults. For Apache CLI,
there are no seeded faults available. But we can capture theprogrammer’s idea of the expected behavior to be in the last
revision 667565 which remains unchanged for the last four
years. This allows us to measure the regression of intermediate
revisions w.r.t. the last revision. For Min, Tcas, and Replace
every difference-revealing test case also reveals a regression.
Answer to RQ2: For the analyzed subjects, PRV generates
a regression-revealing test case on average for 48% moreversion pairs in 63% less time than the eXpress-like approachthat analyzes only the changed version P 0 . The improvementof efficiency over finding a single difference-revealing input(cf. Table I) may be attributed to the subtleness of regression
faults. As an instance of this subtleness, consider the program
versions in Figure 2. The programmer expects that the newversion computes output o = i + 1 instead of o = i for input
i > 0. Otherwise, the behavior shall remain unchanged. Thus,a regression test generation tool may determine progression
for almost 50% of the input (i > 0) but because a branchis evaluated in different directions for i = 0, there exists
regression only for one input. Unintendedly, this input computes different output in the changed version, too. Even thegeneration of an input for every path in the changed program,
like for eXpress, may not produce this test case. In contrast,
differential partitions can capture such subtle differences.
RQ3: Practicability - Usage Scenario: Apache CLIApache CLI is used to evaluate PRV in a practical usage scenario. PRV generates difference-revealing test cases within thebound of 20 minutes for every version pair. A developer checks
these test cases for regression and relates the regressionrevealing test cases to the changes that semantically interfere.
The check is automated in our experiment as illustrated in
Figure 9.b). The expected behavior of CLI is captured by thelast revision (667565) which has not changed in the last four
years and is released in CLI1.1. This allows us to measureprogression and regression w.r.t. to the expected behavior.
The first column in Table III shows the revision pairs, theearlier versus the later revision. The second column presents
the total number of tests generated by PRV followed by the
number of equivalence- and difference-revealing test cases,
respectively. The percentage of difference-revealing test cases(Column 4) witnessing progression (%Progr), regression(%Regr), and the computation of output that has changed
but still does not behave as expected (%Chan) are shown incolumns 5, 6, and 7, respectively.
TABLE IIIE XPLORATION OF DIFFERENTIAL BEHAVIOR IN LIMITED TIME
Subject and Versions #Test #Equ
CLI (20min)

In practice, not every difference-revealing test case reveals
software regression. A difference-revealing test case can bechecked formally or informally against the programmer’s
expectation. In the latter case the programmer looks at theoutput of difference-revealing test cases in both programs andmay know whether the test case reveals regression. Table IIpresents the two aspects measured to find the first regressionrevealing input. The first seven rows show the average time tofind a regression-revealing input per subject. If for a version
pair none of the approaches finds a regression-revealing test
case within the time bound, then it does not contribute to thecalculation of the average time. The mutation score depicts thefraction of versions for which a regression-revealing input canbe found within 20 minutes for Apache CLI and five minutes
for the other subjects.

only P 0
DART-like
eXpress-like307

r129800-r129803
r129803-r129843
r129843-r129849
r129849-r538031
r538031-r667565
Average

788
835
721
509
536

748
809
639
485
455

Difference Revealing#Diff %Progr %Regr %Chan
40
0%
0%
100%
26
65%
0%
35%
82
82%
1%
17%
24
0%
88%
13%
81
100%
0%
0%
49%
18%
33%

Answer to RQ3: For the evolution of Apache CLI over
six years, tests generated as witnesses of differential behaviorof two successive versions suggest an average progression of
49%, regression of 18% and intermediate semantic changesof 33% towards the latest revision. The interested reader may
compare the results in Table III to the developer’s notes in Figure 7. The behavior of CLI generally experiences progression
from version r129800 to r129849 when suddenly the behavior
regresses with the change to r538031. In fact, while trying tofix bug CLI-132 , the developer introduces bug CLI-1373 . Thisis a clear regression bug which is witnessed by 88% of thedifference-revealing test cases generated by PRV. However, ittakes two months to report and twelve to fix bug CLI-137 andcommit it as revision r667565. In contrast, PRV generates thefirst regression-revealing test case for r538031 in 88 seconds
among the first five generated difference-revealing test cases.
V. T HREATS TO VALIDITY
The main threat to internal validity is the correctness of
our implementation of PRV into JSlice. We tried to mitigate
this threat by using the same implementation to gather results
for the DART-like and eXpress-like approaches. In practice,
any implementation of PRV can guarantee the absence ofregression errors to the same extent as symbolic execution
can guarantee the absence of program errors (see e.g., [18]).
Our particular implementation could be faulty, so that it may
not report a witness of behavioral difference if one exists. On
the other hand, a reported witness of behavioral difference isindeed a witness of behavioral difference. This is inherent tothe approach, as the generated test cases are concretely (andsymbolically) executed on both programs.
The main threat to external validity is the generalization of
our results. The limited choice and number of subjects does notsuggest generalizability and serve mainly as comparison to related work and give an idea about the practicability of PRV.
VI. R ELATED W ORK
Regression Verification (RV) is the problem of deciding
whether a changed program is at least as correct as a previous
version. One line of work takes an earlier version as aprogram specification of the new version [1], [2], [33]. The
authors argue if both versions are semantically equivalent,
then there is no software regression. Yet, not every differenceis a regression. For instance, a bug-fix yields anticipatedbehavioral difference. Another line of work requires an explicit
specification, and builds on the full verification of an earlier
version. Subsequently, only the changed behavior of the following versions need to be checked incrementally [34], [35]. In
general, RV can take a long time to terminate. When the searchis interrupted, no intermediate guarantees can be reported. In
contrast, the interruption of PRV can guarantee the absenceof regression at least for the explored equivalence-revealing
partitions. Moreover, the difference-revealing test cases canbe “informally” checked for further regression by developers.
2 https://issues.apache.org/jira/browse/CLI-13

3 https://issues.apache.org/jira/browse/CLI-137

Differential Symbolic Execution (DSE) [30] is a generalapproach to compute program differences while PRV is a specialized approach tailored to RV. Specifically, DSE computes
the differences based on two types of program summaries.
The symbolic summaries in Figure 2 on the right (P and P 0 )precisely characterize the behavior of the program versions
on the left. The abstract summaries in Figure 10 overapproximate the behavior for the same versions. Exploiting thesyntactic similarity of both versions, the behavior of common
code blocks can be represented by uninterpreted functions.
P (=P 0 (=

hP,P 0 i )hP 0 ,P i )Fig. 10.

Input
true
true

Outputo = o(0, i)o0 = o(0, i + 1)

Regression Test Case t
Value for i satisfyingo(0, i) 6= o(0, i + 1)

Program Deltas ( ) and Abstract Summaries (cp. Fig.2)

RV based on program summaries is either less scalable orinfeasible. While symbolic summaries may be used for RV,
the differences are computed as an expensive cross-product of(incomplete) summaries. On the other hand, PRV is based on
differential partitions that account for the common input spaceof both versions. Furthermore, PRV yields coarser partitions.
For instance, if input does not reach a change already implies
both programs compute the same output. Abstract summaries,
on the other hand, remove information required for RV. Theinterested reader may verify in Figure 10 that, if the delta contains uninterpreted functions, a concrete difference-revealing
test case cannot be generated. In this example, each deltaaccounts for a single partition (true), while PRV distinguishes
two difference-revealing and one equivalence-revealing partition. For each partition, PRV generates a witnessing test case.
Regression Test Generation (RTG) is the problem of constructing sample input that can expose software regression.
Classically, test cases are generated towards the coverage ofthe program’s behavior [4], [6]. The hope, when the programis changed and behavior regresses, is that at least one test
case fails in the new version. Further, when the program ischanged, test cases are generated towards the coverage ofprogram elements that are affected by the syntactic changes[11], [12], [36]. These test cases augment an existing test suitethat was coverage-adequate for the earlier version. However,
the analysis of a single program may be insufficient to generatea regression-revealing test case (cf. Fig. 2). Instead, someresearch directly aims at generating difference-revealing test
cases. Syntactic approaches seek to reach a change, infectthe program state, and propagate it to the output [9], [10],[13], [27]. However, the number of possibly semanticallyinterfering sets of changes is exponential to the number ofoverall syntactic changes. Harman et al. [27] note the testingof every subset would be prohibitively expensive. Even fora single subset, the search for a difference-revealing input
may not terminate. In contrast, the number of changes is
unimportant to PRV, à priori. It groups input, depending onwhether it reaches and propagates the same set of changes,
on demand during exploration. More importantly, PRV canguarantee the absence of regression not only for a singularpoint in the common input space, but for an entire partition.

308

VII. C ONCLUSION
Regression testing is probably the most widely used testing
technique. In theory, an adequate regression test suite covers
many semantic elements in a program, that is, different functionalities. The hope is, when the program is changed andexisting functionality stops working as expected, at least one
test case fails. In practice, the adequacy of a regression test
suite is measured in terms of covered syntactic elements in a
program, that is, code coverage. For instance, a test suite is
100% branch coverage-adequate if it exercises every branch.
However, code-coverage may not properly quantify thecapability of a test suite to reveal regression errors, as Böhme
motivates in [37]. While syntactic coverage is a practical approximation of semantic coverage, it remains unclear whether
a Coverage-adequate Test Suite (CaTS) performs significantly
better in terms of revealing errors than the execution of random
input [38], [39]. Weyuker et al. [4] argue that any (failing) test
case in a CaTS may not be representative of (the observed)
errors. Moreover, even if all CaTS tests execute successfully,that shall not inspire confidence in correctness [5].
We propose the exploration of differential partitions togroup input with the same “differential behavior”. As such,
each generated test case becomes significant and representativeof a larger set of inputs. Once a test case is executed on bothversions and exposes a difference, PRV can soundly generalize
to those inputs that are also difference-revealing. This allows toassess the adequacy of a test suite not in terms of the covered
code elements but the covered input space. PRV shall inspire
confidence in the absence of regression at least for input in the
covered input space - establishing a form of “comfort zone”.
Experiments show that PRV exposes regression errors thatare not detected by other regression test generation methods.
In summary, differential partitions enable a gradual andpartial form of regression verification. Differential partitions
exist as a unit of verification in the common input space oftwo program versions and are checked one after another. Whenthe verification process is interrupted, PRV retains regression
guarantees for the explored input space. This is crucial as
verifying the complete input space is prohibitively expensive.
ACKNOWLEDGMENT
This work was partially supported by Singapore’s Ministryof Education research grant MOE2010-T2-2-073.
R EFERENCES[1] B. Godlin and O. Strichman, “Regression verification: proving theequivalence of similar programs,” Softw. Test., Verif. Reliab., pp. 1–18,
March 2012. [Online]. Available: http://dx.doi.org/10.1002/stvr.1472[2] S. Chaki, A. Gurfinkel, and O. Strichman, “Regression verification for
multi-threaded programs,” in VMCAI, 2012, pp. 119–135.
[3] J. C. King, “Symbolic execution and program testing,” Commun. ACM,
vol. 19, no. 7, pp. 385–394, Jul. 1976.
[4] E. J. Weyuker and B. Jeng, “Analyzing partition testing strategies,” IEEE
Trans. Softw. Eng., vol. 17, no. 7, pp. 703–711, Jul. 1991.
[5] D. Hamlet and R. Taylor, “Partition testing does not inspire confidence(program testing),” IEEE Trans. Softw. Eng., vol. 16, no. 12, pp. 1402–
1411, Dec. 1990.
[6] P. Godefroid, N. Klarlund, and K. Sen, “Dart: directed automatedrandom testing,” in PLDI, 2005, pp. 213–223.

[7] D. Qi, H. D. Nguyen, and A. Roychoudhury, “Path exploration basedon symbolic output,” in ESEC/SIGSOFT FSE, 2011.
[8] D. Beyer, T. A. Henzinger, M. E. Keremoglu, and P. Wendler, “Conditional model checking: a technique to pass information between
verifiers,” in FSE, 2012, pp. 57:1–57:11.
[9] B. Korel and A. M. Al-Yami, “Automated regression test generation,”in ISSTA, 1998, pp. 143–152.
[10] D. Qi, A. Roychoudhury, and Z. Liang, “Test generation to expose
changes in evolving programs,” in ASE, 2010, pp. 397–406.
[11] S. Person, G. Yang, N. Rungta, and S. Khurshid, “Directed incremental
symbolic execution,” in PLDI, 2011, pp. 504–515.
[12] K. Taneja, T. Xie, N. Tillmann, and J. de Halleux, “express: guided path
exploration for efficient regression test generation,” in ISSTA’11.
[13] R. Santelices, P. K. Chittimalli, T. Apiwattanapong, A. Orso, and M. J.
Harrold, “Test-suite augmentation for evolving software,” in ASE, 2008.
[14] H. Agrawal, J. R. Horgan, E. W. Krauser, and S. London, “Incremental
regression testing,” in ICSM, 1993, pp. 348 – 357.
[15] T. Gyimóthy, A. Beszédes, and I. Forgács, “An efficient relevant slicing
method for debugging,” in ESEC/SIGSOFT FSE, 1999, pp. 303–321.
[16] G. L. Thione and D. E. Perry, “Parallel changes: Detecting semanticinterferences,” in COMPSAC, 2005, pp. 47–56.
[17] M. Böhme, B. C. d. S. Oliveira, and A. Roychoudhury, “Partition-based
regression verification,” National University of Singapore, Tech. Rep.
TRB8/12, ’12, http://www.comp.nus.edu.sg/⇠mboehme/PRV-TR12.pdf.
[18] N. E. Beckman, A. V. Nori, S. K. Rajamani, and R. J. Simmons, “Proofs
from tests,” in ISSTA ’08, pp. 3–14.
[19] P. Boonstoppel, C. Cadar, and D. R. Engler, “Rwset: Attacking path
explosion in constraint-based test generation,” in TACAS, 2008, p. 351.
[20] M. Delahaye, B. Botella, and A. Gotlieb, “Explanation-based generalization of infeasible path,” in ICST, 2010, pp. 215 –224.
[21] M. Staats and C. S. Pasareanu, “Parallel symbolic execution for structural test generation,” in ISSTA, 2010, pp. 183–194.
[22] J. Malburg and G. Fraser, “Combining search-based and constraint-based
testing,” in ASE, 2011, pp. 436–439.
[23] P. McMinn, M. Harman, D. Binkley, and P. Tonella, “The species perpath approach to searchbased test data generation,” in ISSTA, 2006, pp.
13–24.
[24] T. Wang and A. Roychoudhury, “Using compressed bytecode traces forslicing Java programs,” in ICSE, 2004, pp. 512–521.
[25] L. M. de Moura and N. Bjørner, “Z3: An efficient smt solver,” in TACAS,
2008, pp. 337–340.
[26] A. J. Offutt and J. Pan, “Automatically detecting equivalent mutants andinfeasible paths,” Softw. Test., Verif. Reliab., vol. 7, pp. 165–192, 1997.
[27] M. Harman, Y. Jia, and W. B. Langdon, “Strong higher order mutationbased test data generation,” in ESEC/SIGSOFT FSE, 2011, pp. 212–222.
[28] K. Taneja, T. Xie, N. Tillmann, J. de Halleux, and W. Schulte, “Guided
path exploration for regression test generation,” in ICSE Companion,
2009, pp. 311–314.
[29] W. Jin, A. Orso, and T. Xie, “Automated behavioral regression testing,”
in ICST, 2010, pp. 137–146.
[30] S. Person, M. B. Dwyer, S. G. Elbaum, and C. S. Pasareanu, “Differential
symbolic execution,” in SIGSOFT FSE, 2008, pp. 226–237.
[31] H. Do, S. G. Elbaum, and G. Rothermel, “Supporting controlled experimentation with testing techniques: An infrastructure and its potential
impact.” Empir. Softw. Eng., vol. 10, no. 4, pp. 405–435, 2005.
[32] Z. Yin, D. Yuan, Y. Zhou, S. Pasupathy, and L. N. Bairavasundaram,“How do fixes become bugs?” in SIGSOFT FSE, 2011.
[33] S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebêlo, “Symdiff: A
language-agnostic semantic diff tool for imperative programs,” in CAV,
2012, pp. 712–717.
[34] G. Yang, M. B. Dwyer, and G. Rothermel, “Regression model checking,”
in ICSM, 2009, pp. 115–124.
[35] S. Lauterburg, A. Sobeih, D. Marinov, and M. Viswanathan, “Incremental state-space exploration for programs with dynamically allocateddata,” in ICSE, 2008, pp. 291–300.
[36] Z. Xu, Y. Kim, M. Kim, G. Rothermel, and M. B. Cohen, “Directed test
suite augmentation: techniques and tradeoffs,” in FSE ’10, pp. 257–266.
[37] M. Böhme, “Software regression as change of input partitioning,” in
ICSE, 2012, pp. 1523–1526.
[38] J. W. Duran and S. C. Ntafos, “An evaluation of random testing,” IEEE
Trans. Softw. Eng., vol. 10, no. 4, pp. 438 –444, July 1984.
[39] A. Arcuri, M. Z. Iqbal, and L. Briand, “Random testing: Theoreticalresults and practical implications,” IEEE Trans. Softw. Eng., vol. 38,
no. 2, pp. 258–277, 2012.

309