SOURCE ARCHIVE
EXTRACTED CONTENT
41,243 charsGenerating Distinguishing Tests using the MINION Constraint Solver
Franz Wotawa and Mihai Nica and Bernhard K. Aichernig Institute for Software Technology Technische Universit¨at Graz, Graz, Austria Email: {wotawa,nica,baichern}@ist.tugraz.at
Abstract—We discuss the generation of test cases for demon- Before discussing our technique for generating distinguish-
strating the non-equivalence of two programs. This problem has ing test cases in detail, we outline the underlying ideas on a
applications in mutation testing and automated debugging. After small example program. More details are given in the rest of
transforming the programs into Static-Single-Assignment form,
the MINION constraint solver is used to generate test vectors that this paper.
demonstrate the observable difference. The experiments show the 1. begin
feasability of our constraint solving approach. 2. i = 2 * x;
I. INTRODUCTION 3. j = 2 * y;
Constraints have been used for various purposes like verifi- 4. o1 = i + j;
cation [4], debugging [2], [13], program understanding [14] as 5. o2 = i * i;
well as testing [6], [9], [10]. Some of the proposed techniques 6. end;
use constraints to state specification knowledge like pre- and This program can be easily converted into a constraint
post-conditions. Others use constraints for modeling purposes representation using the constraint language from MINION. or extract the constraints directly from the source code. In We only need to convert the program statement by statement. this paper we rely on the latter and use constraints obtained For representing constraints we use a relational notation. For from the program directly. In contrast to previous research we example, the multiplication x ∗ y = z is represented by focus on generating test cases that can be used to distinguish- product(x,y,z) and for the sum x+y = z we use the two ing different implementations. A test case distinguishes two relations sumleq([x,y],z) and sumgeq([x,y],z) implementations if it reveals a different output behavior using stating x + y ≤ z and x + y ≥ z respectively. Hence, the the same inputs for both implementations. Of course such a constraint representation of our program is the following: distinguishing test case might not exists always. Moreover, product(2,x,i) we assume that the implementations behave deterministically. product(2,y,j) Otherwise, it is not guaranteed that a given input always sumleq([i,j],o1) generates the same outputs. sumgeq([i,j],o1) There are many potential applications of distinguishing test product(i,i,o2) cases. The first application scenario is test case generation based on program mutations. In such an application mutants Now consider a variant of the program where Line 3 is for a given program are generated. The distinguishing test changed to j = 3*y and let us again convert it into its case generator is used to compute test cases for each mutant constraint representation. Note that in this case we added a and the original program. The other scenario is debugging. In post-fix string ” v” to each variable to distinguish the variables debugging we might obtain too many diagnosis candidates, of the original program from the variables of the variant. i.e., parts of the program that explain a detected misbehavior. product(2,x_v,i_v) In order to reduce the diagnosis candidates we have to add product(3,y_v,j_v) new information like test cases. The distinguishing test case sumleq([i_v,j_v],o1_v) generator delivers this new test cases. sumgeq([i_v,j_v],o1_v) The idea behind our approach is to convert two imple- product(i_v,i_v,o2_v) mentations into constraints and to represent the problem of generating distinguishing test cases as constraint satisfaction Informally speaking a distinguishing test case is a test case problem. In order to convert a program into a constraint system for separating the behavior of two programs where the input we first remove the loops and iterations by replacing them values for each program is the same but the computed output basically with a bounded sequence of conditionals. Then we is not. Hence, we have to state that the inputs are the same compile the resulting program into its static single assignment and that there exists at least one output where the computed form from which we are able to compute the constraints values are not equivalent. Using the MINION constraint eq directly. For the constraint representation and the solving we for stating equivalence, diseq for stating that two variables rely on the MINION constraint solver [8], [11]. are inequivalent, and the logical constraint watched-or for
formalizing a disjunction, we give the constraints necessary to
obtain a distinguishing test case in our example: (I, ∅) is distinguishing Π from Π′ ⇔
eq(x,x_v) ∃ x : (x, v) ∈ Π(I ) ∧ (x, v′) ∈ Π′(I ) ∧ v = v′
eq(y,y_v) We call the problem of finding an input environment that
watched-or({diseq(o1,o1_v),diseq(o2,o2_v)}) distinguishes two programs Π and Π′ the distinguishing test A solution for the given constraints is also a distinguishing case problem. It is worth noting that a distinguishing test test case. Using MINION as constraint solver we are able case is according to our definitions always a passing test case to compute more than one distinguishing test cases for this because the output environment is not specified. From the example, e.g., one solution is x=2, y=2 and there are many distinguishing test case we always are able to derive a test case others. All solutions have in common that y is not equal to 0. with a specified expected output. This can be done manually The rest of this paper is organized as follows. In the next or in some cases automatically. The latter is used to compute section we discuss the program conversion step and give test cases from the mutations of a given program. In this case all necessary basic definitions. Afterwards, we outline the the program is assumed to be correct and the output of the algorithm for computing distinguishing test cases and present execution of the program is therefore the expected output of first empirical results. Finally, we discuss related research and the test case. When searching for distinguishing test cases for conclude the paper. all mutants we finally receive a test suite that can be used to II. BASIC DEFINITIONS separate the original program from all its mutations. We assume that the program Π to be compiled into a A. Conversion of programs to constraints constraint representation is deterministic and written in an The problem of computing distinguishing test cases can imperative assignment language with the usual kinds of state- be reduced to a constraint satisfaction problem (CSP). The ments, e.g., variable assignments, conditional statements, and only requirement is that we are able to compile programs loops. The underlying type system of the language comprises into an equivalent constraint representation. Based on previous basic datatypes like Booleans, integers, floating point numbers work [4], [7] and to be self contained we briefly discuss this and arrays. Each variable stores a value of the corresponding compilation process. datatype. The values of variables are stored in a variable Our work addresses sequential programs with a syntax environment. A variable environment (or environment for and semantics similar to well-known languages like Java, but short) is a function mapping variables to their values. We without object-oriented constructs. For simplicity we do not further assume that each program Π has some input variables consider procedure calls and arrays in this paper, but it should and output variables. We use Π(I ) to denote execution of be noted that procedures and arrays can be straightforwardly Π on a specific input environment (or input for short) I . integrated as shown in ([13]). Our approach supports assign- The result of the execution is always an environment, i.e., ment statements, conditional statements, and loops. Figure 1 the output environment. In the following we also represent depicts a program which serves as running example throughout environments as set of tuples (x, v) where x is a variable and the rest of the paper. v is a value. A test case is a tuple (I, O) where I is the input environment int power(int a, int exp) denoting the given values of input variables, and O is the 1. int e = exp; output environment where the expected values of the output 2. int res = 1; variables are specified. Note that regarding the definition it is 3. while (e > 0) { also possible that O is empty. A program Π is passing a test 4. res = res * a; case (I, O) if and only if the execution of Π on I returns the 5. e = e - 1; } expected output values specified in O. Formally, we define 6. return res; passing and failing as follows: Fig. 1. A program for computing aexp, where a and exp are integers. Variable res denotes the result. Π(I ) ⊇ O ⇔ Π passes test case(I, O) ¬(Π passes test case(I, O)) ⇔ Π fails test case(I, O) As loops cannot be directly converted to our constraint representation, past works have proposed to unroll loops, i.e., Note that not all values have to be specified. However, it to create a loop-free program by replacing the loop of the is necessary that all given values are returned as expected. A original program by a set of nested if-statements (e.g., see variable where no value is specified in O can have an arbitrary [2] and [13]). If the maximum number of iterations is known value after program execution. in advance, then the loop-free program is equivalent to the Definition 1 (Distinguishing test case): Given programs Π original program. Note that in our case we are able to restrict and Π′. A test case (I, ∅) is a distinguishing test case if the number of loops searching for distinguishing test cases and only if there is at least one output variable where the within the given maximum number of iterations. Figure 2 value computed when executing Π is different from the value shows the loop-free version of our example program for 2 computed when executing Π′ on the same input I . iterations.
int power_loopfree(int a, int exp) int power_SSA(int a, int exp)
1. int e = exp; 1. int e_0 = exp;
2. int res = 1; 2. int res_0 = 1;
3. if (e > 0) { 3. bool cond_0 = (e_0 > 0);
4. res = res * a; 4. int res_1 = res_0 * a;
5. e = e - 1; 5. int e_1 = e_0 - 1;
6. if (e > 0) { 6. bool cond_1 = cond_0 ∧ (e_1 > 0);
7. res = res * a; 7. int res_2 = res_1 * a;
8. e = e - 1; 8. int e_2 = e_1 - 1;
9. return res; 9. int res_3 = Φ(res_2, res_1, cond_1);
} } 10. int e_3 = Φ(e_2, e_1, cond_1);
11. int res_4 = Φ(res_3, res_0, cond_0);
Fig. 2. The loop-free version of the program in Fig. 1 for 2 iterations. 12. int e_4 = Φ(e_3, e_0, cond_0);
Our constraint representation requires that all left-side vari- Fig. 3. The loop-free SSA form of the program in Fig. 1 for 2 iterations. Variable res_4 is the output of the program (i.e., the final result). ables in the program have unique names, i.e., each variable should be defined only once. Hence, we use the Static Single Assignment (SSA) form, which is an intermediate represen- x_j = E1expr; tation of the program with the property that no two left- x_k = E2expr; side variables have the same name (see [3], [1], [12]). This x_l = Φ(x_j, x_k, cond_i); is achieved by replacing each left-side variable with a new variable whose name is composed of the name of the original The SSA representation for the program in Fig. 1 is depicted variable plus a unique index as suffix, see Fig. 3. in Fig. 3. A noteworthy statement is: In order to obtain the SSA form of a program it is also nec- 6. bool cond_1 = cond_0 ∧ (e_1 > 0); essary to convert loops and conditional statements. As loops The variable cond_1 is true iff e > 0 holds in the original are, in our approach, represented by nested if-statements, we program after the first loop iteration, i.e., cond_1 is true iff only need to consider the conversion of conditional statements a second loop iteration is executed. This is the case iff e_0 of the form > 0 and e_1 > 0 holds. if(condexpr) then {...} else {...} Obviously, the conversion of the loop-free program into the Note that the notation xexpr denotes a whole expression rather SSA form has, apart from variable renaming, no influence on than a single variable. In brief, this conversion works as the actual program behavior. It can also be seen that the SSA follows: form of a sequential program comprises only assignments of
- The value of the evaluated condition condexpr is stored the general form
in a new boolean variable cond_i, where i is a unique v = Eexpr
- index. where v is a variable and Eexpr is either an expression in the The if- and the else-branches are converted sepa- syntax of the sequential language or it is an expression of the rately. For both branches, new variables with unique form Φ(...). indexes are introduced. The statements of both branches What is missing in the conversion process is the mapping are concatenated; i.e., the program in SSA form will of SSA programs to MINION constraints. MINION offers
- execute the statements of either branch in every run. support for almost all arithmetics, relational, and logic opera- New variables are added which have the value of the tors like minus, plus, multiplication, division, less, and equal corresponding variables in the original program after the over integers, but enforces all expressions used in a MINION execution of the if- or else-branch, respectively. The program to be limited to one operator. values of these new variables depend on the indexed Because of the syntactical limitations of MINON we have variables which were introduced for the branches and to convert an assignment statement with an expression E on the boolean condition condexpr. For the evaluation expr of those values we define the Φ-function: on the right-side comprising more than one operator into a def v k otherwise version is simple. A constant or variable is represented by Φ(v j, v k, cond i) = { v j if cond i = true sequence of MINON statements. The idea behind the con- itself. For an expression of the form E1expr op E2expr we convert For example, the corresponding SSA form of the program E 1 expr and E2expr separately, and assign a new intermediate
fragment variable for each converted sub-expression. The following
if(condexpr) {x = E1expr;} else {x = E2expr;} ComputeExpression algorithm implements the conversion.
is given as follows: Algorithm ComputeExpression(Eexpr)
Input: An expression Eexpr and an empty set M for storing
cond_i = condexpr; the MINION constraints.
Output: A set of minion constraints representing the expres- 4) Rename all variables x used in constraints M2 to x_P2.
sion stored in M , and a variable or constant where the result 5) Let M be M1 ∪ M2.
of the conversion is finally stored. 6) For all input variables x ∈ IN do:
1) If Eexpr is a variable or constant, then return Eexpr. a) Add the constraint eq(x_P1, x_P2) to M .
2) Otherwise, Eexpr is of the form E1expr op E2expr. 7) For all output variables x ∈ OU T do:
3) Let aux1 = ComputeExpression (E1expr) a) Add the constraint diseq(x_P1, x_P2) to M .
4) Let aux2 = ComputeExpression (E2expr) 8) Return the values of the input variables obtained when
5) Generate a new MINON variable result and create calling the MINION constraint solver on M as result.
MINON constraints accordingly to the given operator
op, which define the relationship between aux1, aux2, The computeDistinguishingTest algorithm obviously termi-
and result, and add them to M . nates. The given programs and sets are all finite and the
6) Return result. conversion terminates. Moreover, the constraint solver also ter-
For example, the expression a_0 + b_0 - c_0 is con- minates after checking all possible solutions when considering verted to the following MINION constraints using Compute- only finite domains. The computational complexity is mainly Expression where aux1 and aux2 represent new variables determined by the constraint solver. The conversion itself is introduced during conversion. polynomial in the size of the programs. Finding a solution for a finite domain is exponential in the number of used variables. sumleq([a_0,b_0],aux1) Note that the whole approach is not necessary restricted sumgeq([a_0,b_0],aux1) to the MINION constraint solver. All discussed steps can be weightedsumleq([1,-1],[aux1,c_0], aux2) adapted to other constraint solvers. In the following section, we weightedsumgeq([1,-1],[aux1,c_0], aux2) present first empirical results of the approach using MINION. In this example the MINION constraints sumleq and IV. EXPERIMENTAL RESULTS sumgeq are used to represent the plus operator, and We implemented the discussed approach in Java and applied weightedsumleq and weightedsumgeq together with it on some small Java programs ignoring object-oriented the given list of signs are for representing the minus operator. features. For each program we have the original bug-free We summarize the conversion of the SSA statements to version, and a set of four mutants obtained by manually MINION constraints in Table I using some of the statements injecting different single-faults into the original program. Each from the example given in Fig. 3. program comprises at least one loop structure. We generate For convenience we assume a function convert that imple- the discriminating test cases, i.e., kill the mutants, considering ments the conversion of programs into MINION constraints as 2, 4 and 7 iterations of each loop statement. We present discussed in this section. Hence, convert takes the number of the obtained results in Table II. All the experiments were necessary iterations for each while-statement and the program performed using an Intel Pentium Dual Core 2 GHz computer as input and returns a set of MINION constraints as output. with 4 GB RAM. We imposed a limit of two hours in which We use this function in the next section, where we discuss an the mutant should be killed and a distinguishing test case have algorithm for computing distinguishing test cases. to be computed. In our experiments no out-of memory error III. COMPUTING DISTINGUISHING TEST CASES was encountered. All variables from the tested programs are In order to compute distinguishing test cases for two pro- either of type boolean or of type integer. All integer variables grams Π1 and Π2 we have to ensure that the inputs for both are defined over the finite discrete domain [−250 . . . 250]. programs are the same whereas the computed outputs are In some cases the inserted fault lead to an infinite execution different. This idea can be easily represented in MINION. of the loop structure, e.g., replacing a minus with a plus in a We only have to add the corresponding constraints to the while-structure. Due to the fact that our analysis is based on converted programs. Moreover, we have to ensure that the a static representation of the programs using a fixed number converted programs use different names for the variables. of iterations, the constraint solver is still able to compute an Hence, we have to rename the variables in the constraint output that satisfies the requirements. But when executing the representation before putting them together. The following program and its mutant, the mutant will never stop. Hence, algorithm computeDistinguishingTest takes care of all of the our approach does not require to check program termination requirements. for computing test cases. Algorithm computeDistinguishingTest (Π1,Π2, #It) Another limitation of this approach is that there is no guar- Inputs: Two programs Π1 and Π2 having the same input antee for computing a solution, i.e., a test case that kills the variables (IN ) and output variables (OU T ), and a maximum mutant. In order to identify a faulty statement both the original number of iterations #It. and its mutant must execute that faulty statement. However Outputs: A distinguishing test case. there are situations when the faulty statement does not have an influence over the output. In this case a distinguishing test 1) Call convert(Π1,#It) and store the result in M1. case cannot be determined. 2) Call convert(Π2,#It) and store the result in M2. One problem we faced in our experiments was the time 3) Rename all variables x used in constraints M1 to x_P1. needed for computing a solution for some examples. See
SSA Statement MINION Constraint
int e 0 = exp; auxVar = ComputeExpression(exp),
eq(e 0, auxVar)
bool cond 0 = (e 0 > 0); reify(ineq(0,e 0,-1 ),cond 0)
bool cond 1 = cond 0 ∧ (e 1 > 0); reify(ineq(0,e 1,-1 ),cond aux)
reify(watchsumgeq([cond 0,cond aux], 2),cond 1)
int res 4 = Φ(res 3, res 0, cond 0); watched-or(eq(cond 0,0), eq(res 4,res 3)) watched-or(eq(cond 0,1), eq(res 4,res 0))
TABLE I
MINION CONSTRAINTS CONVERSION
for example the results of program GcdATC in Table II recently, colleagues in Oxford use the CBMC model checker where MINION was not able to compute a solution for the to generate distinguishing test cases from non-deterministic versions V3 and V4 within 2 hours. The reason was the C code generated from Matlab/Simulink [22]. In contrast to huge search space and the fact that no variable ordering was our test case generator, CBMC relies on SAT-solving and imposed. However, after applying a variable ordering where a different intermediate representation of the programming variables are ordered with respect to their first definition in language. the program, the situation changed. When using the variable The closest work to ours is [9], [10]. In these papers ordering MINION had no problem in killing them in less than the authors described the use of constraint solving for test a second. Due to this particularity, in our approach we always case generation. They also make use of similar conversion impose an ordering over the input and output variables. Note techniques. In contrast to the previous work we are focusing on that for programs of reduced complexity the variable ordering computing distinguishing test cases to be used for debugging leads to no gains with respect to time performances. and also for test case generation based on program mutations. The obtained results are very promising but further studies have to be performed. In particular, generating test cases for VI. CONCLUSION larger programs comprising several thousands lines of code In this paper we introduced an approach for generating and the ability to handle object-oriented constructs are of distinguishing test cases based on constraint satisfaction prob- interest. lems. A distinguishing test case for two programs is a test V. RELATED RESEARCH case that reveals different values for the output variables of the programs when using the same input. The application areas are As already mentioned our distinguishing test cases play an automated test case generation based on program mutations essential role in mutation testing. The distinguishing test cases and fault localization. With respect to mutation testing, the are those who are able to kill a given mutant. However, in distinguishing test cases serve the following purposes: The classical mutation testing, the distinguishing test cases are not tests are defined to kill the set of known mutants, which generated, but a given test suite is assessed with respect to its would not be useful in itself. However, these test cases (1) ability of distinguishing all mutants, i.e. to find all injected can be used as a basis for further regression testing, (2) they faults [20], [19]. It would not be useful to inject faults and guarantee a certain coverage in the code (it is well-known that then generate a distinguishing test case to find these known mutation coverage subsumes classical coverage criteria, like faults. However, the idea found application in model-based e.g. branch coverage), (3) via the mutation testing assumption mutation testing, where distinguishing test cases are generated of the coupling effect, these test cases will detect more from mutated models and then executed on an implementation. subtitle faults in the program. With respect to fault localization Very early, Tai and Su [23] proposed algorithms for generating distinguishing test cases are of interest for reducing the number test cases that guarantee the detection of Boolean operator of fault candidates. errors in electronic circuits. Beside the theory and technique behind our approach we Our group used different modeling styles and tools to gen- present first empirical results using MINION as the underlying erate the distinguishing test cases: for OCL pre-postcondition constraint solver. The results are promising and the time contracts a constraint-solver was used [18], for Spec# contracts required for computing a test case can be neglected. Even we exploited Microsoft’s Z3 SMT-solver [21], for LOTOS in the case of 1,500 constraints and almost 1,000 variables protocol specifications first a bisimulation checker [16], then the time required for computing a test case was less than 4 an ioco-conformance checker [24] was applied, and finally seconds. model checkers served to generate distinguishing test cases for embedded systems [25] and REO coordination models [15]. ACKNOWLEDGEMENT None of these papers considered programs. The work described in the paper was partially funded by the In our theory of mutation testing, we also covered test case Austrian Science Fund (FWF) under contract number P20199- generation for programs [17]. However, in this work a different N15, and the EU FP7 project MOGENTES ICT-216679, normal form for the constraint solver was proposed. Which Model-based Generation of Tests for Dependable Embedded one is more efficient is open to future experiments. Most Systems.
Name LOC #I/O #It2 V1 V2 V3 V4 #CO #VarCO Killed (0,07s) Killed(0,06s) Killed(0,04s) Killed(0,03s) 47 32 MultATC 12 2/1 4 Killed (0,04s) Killed(0,08s) Killed(0,07s) Killed(0,07s) 87 56 7 Killed (0,01s) Killed(0,10s) Killed(0,11s) Killed(0,11s) 151 92 2 Killed (0,4s) Killed(0,03s) Killed(0,4s) Killed(0,4s) 49 34 SumATC 13 2/1 4 Killed (0,4s) Killed(0,07s) Killed(0,49s) Killed(0,47s) 89 58 7 Killed (0,67s) Killed(0,11s) Killed(0,62s) Killed(0,09s) 149 94 2 Killed (0,2s) Killed(0,12s) Killed(0,21s) Killed(0,18s) 132 86 MultV2ATC 18 2/1 4 Killed (0,34s) Killed(0,23s) Killed(0,31s) Killed(0,31s) 418 258 7 Killed (2,09s) Killed(2,09s) Killed(2,15s) Killed(2,15s) 1144 696 2 Killed (0,06s) Killed(0,06s) Killed(0,06s) Killed(0,06s) 65 52 DivATC 22 2/1 4 Killed (0,08s) Killed(0,08s) Killed(0,6s) Killed(0,08s) 105 76 7 Killed (0,10s) Killed(0,10s) Killed(0,09s) Killed(0,12s) 165 112 2 Killed (0,07s) Killed(0,35s) Killed(46s/0,6s) X/Killed(0,15s) 126 90 GcdATC 24 2/1 4 Killed (0,08s) Killed(0,08s) X/Killed(0,12s) X/Killed(0,5s) 206 138 7 Killed (0,10s) Killed(0,10s) X/Killed(0,4s) X/Killed(0,65s) 333 220 2 Killed (0,25s) Killed(0,25s) Killed(0,24s) Killed(0,24s) 303 213 RandomATC 52 3/1 4 Killed (0,8s) Killed(0,8s) Killed(0,8s) Killed(0,8s) 667 433 7 Killed (3,5s) Killed(3,47s) Killed(3,6s) Killed(3,59s) 1513 943
TABLE II
FOR EACH PROGRAM NAME, LOC IS THE NUMBER OF STATEMENTS IN THE ORIGINAL PROGRAM, #I/O REPRESENTS THE NUMBER OF INPUTS AND
OUTPUTS INVOLVED IN THE GENERATED TEST CASE, #IT REPRESENTS THE NUMBER OF ITERATIONS FOR THE LOOP-UNROLLING, V1,V2,V3 AND V4
DESIGNATE FOUR DIFFERENT MUTANTS OF THE PROGRAM, #CO DESIGNATES THE NUMBER OF MINION CONSTRAINTS WHEREAS #VarCO
DESIGNATES THE NUMBER OF VARIABLES ASSOCIATED TO THE MINION CONSTRAINT SYSTEM. THE TABLE INDICATES THE TIME NECESSARY TO
IDENTIFY A SUITABLE TEST CASE, ABLE TO ”KILL” THE MUTANT. X STANDS FOR NOT BEING ABLE TO KILL THE MUTANT WITHIN LESS THAN 2 HOURS
.
REFERENCES [15] Bernhard K. Aichernig, Farhad Arbab, Lacramioara Astefanoaei,
Frank S. de Boer, Sun Meng, and Jan Rutten. Fault-based test case
[1] M. M. Brandis and H. M¨ossenb¨ock. Single-pass generation of static generation for component connectors. In TASE 2009, Third IEEE
assignment form for structured languages. ACM TOPLAS, 16(6):1684– International Symposium on Theoretical Aspects of Software Engineering,
1698, 1994. Tianjin, China, July 29–31, pages 147–154. IEEE Computer Society, July
[2] R. Ceballos and R. M. Gasca and C. Del Valle and D. Borrego. [16] 2009. Copyright by IEEE. Diagnosing Errors in DbC Programs Using Constraint Programming. Bernhard K. Aichernig and Carlo Corrales Delgado. From faults via Lecture Notes in Computer Science, Vol. 4177, Pages 200-210, 2006. test purposes to test cases: on the fault-based testing of concurrent [3] R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. Kenneth systems. In Luciano Baresi and Reiko Heckel, editors, Proceedings Zadeck. Efficiently computing static single assignment form and the of FASE’06, Fundamental Approaches to Software Engineering, Vienna, control dependence graph. ACM TOPLAS, 13(4):451–490, 1991. Austria, March 27–29, 2006, volume 3922 of Lecture Notes in Computer [4] H. Collavizza and M. Rueher. Exploring Different Constraint-Based [17] Science, pages 324–338. Springer-Verlag, 2006. Modelings for Program Verification. In Principles and Practice of Bernhard K. Aichernig and Jifeng He. Mutation testing in UTP. Formal Constraint Programming (CP 2007), pages 49–63,Providence, RI, USA, Aspects of Computing, 21(1-2):33–64, February 2009. Copyright owned September 2007. [18] by BCS. The original publication is available at springerlink.com. Bernhard K. Aichernig and Percy Antonio Pari Salas. Test case [5] R. Dechter. Constraint Processing. Morgan Kaufmann, 2003. generation by OCL mutation and constraint solving. In Kai-Yuan Cai and [6] R. A. DeMillo and A. J. Offutt Constraint-based Automatic Test Data Atsushi Ohnishi, editors, QSIC 2OO5, Fifth International Conference on Generation IEEE Transactions on Software Engineering, 17(9):900-910, Quality Software, Melbourne, Australia, September 19-21, 2005, pages September 1991. 64–71. IEEE Computer Society Press, 2005. [7] Tristan Denmat, Arnaud Gotlieb and Mireille Ducass´e, Proving or Dis- [19] R. DeMillo, R. Lipton, and F. Sayward. Hints on test data selection: proving likely Iniants with Constraint Reasoning, In Proceedings of the Help for the practicing programmer. IEEE Computer, 11(4):34–41, April 15th Workshop on Logic-based methods in Programming Environments 1978. October 2005, Sitges, Spain. [20] Richard G. Hamlet. Testing programs with the aid of a compiler. IEEE [8] I. P. Gent, C. Jefferson, I. Miguel. MINION: A Fast, Scalable, Constraint Transactions on Software Engineering, 3(4):279–290, July 1977. Solver. 17th European Conference on Artificial Intelligence (ECAI-06). [21] Willibald Krenn and Bernhard K. Aichernig. Test case generation by Riva del Garda, Italy, 2006. contract mutation in Spec#. In Proceedings of Fifth Workshop on Model [9] A. Gotlieb and B. Botella and M. Rueher. Automatic Test Data Generation Based Testing (MBT 2009), York, England, 22 March 2009, volume 253 using Constraint Solving Techniques. In Proceedings of the International (2) of Electronic Notes in Theoretical Computer Science, pages 71–86. Symposium on Software Testing and Analysis (ISSTA). 1998. Elsevier, October 2009. [10] A. Gotlieb and B. Botella and M. Rueher. A CLP Framework for [22] Daniel Kroening. Automated test-case generation for simulink. Pre- Computing Structural Test Data. In Proceedings of the International sentation at FMCO 2009, Software Technologies Concertation on Formal Conference on Computational Logic (CL). pp 399–413, Springer LNAI Methods for Components and Objects, Nov. 4–5, Eindhoven, The Nether- 1861, 2000. lands, November 2009. [11] MINION, 2009. http://minion.sourceforge.net. [23] K.-C. Tai and H.-K. Su. Test generation for Boolean expressions. In [12] M.N. Wegman and F.K. Zadek. Constant propagation with conditional Proceedings of the Eleventh Annual International Computer Software and branches. ACM Transactions on Programming Languages and Systems, [24] Applications Conference (COMPSAC), pages 278–284, 1987. 13(2), April 1991. Martin Weiglhofer, Bernhard Aichernig, and Franz Wotawa. Fault-based [13] F. Wotawa, M. Nica. On the Compilation of Programs into their conformance testing in practice. International Journal of Software and equivalent Constraint Representation. In Informatica Journal, Volume [25] Informatics, 3(2–3):375–411, June/September 2009. 32, pages 359-371, 2008. G. Fraser and F. Wotawa. Mutant Minimization for Model-Checker [14] S. Woods and Q. Yang, Q, Program Understanding as Constraint Based Test-Case Generation. In Testing: Academic and Industrial Con- Satisfaction: Representation and Reasoning Techniques, Automated ference Practice and Research Techniques - MUTATION (TAICPART- Software Engineering, 5(2):147-181, April 1998. MUTATION). pp. 161 - 168, 2007.