Identifying method-level mutation subsumption relations using Z3

Context: Mutation analysis is a popular but costly approach to assess the quality of test suites. One recent promising direction in reducing costs of mutation analysis is to identify redundant mutations, i.e., mutations that are subsumed by some other mutations. A previous approach found redundant mutants manually through truth tables but it cannot be applied to all mutations. Another work derives them using automatic test suite generators but it is a time consuming task to generate mutants and tests, and to execute tests.Objective: This article proposes an approach to discover redundant mutants by proving subsumption relations among method-level mutation operators using weak mutation testing.Method: We conceive and encode a theory of subsumption relations in the Z3 theorem prover for 37 mutation targets (mutations of an expression or statement). Results: We automatically identify and prove a number of subsumption relations using Z3, and reduce the number of mutations in a number of mutation targets. To evaluate our approach, we modified MuJava to include the results of 24 mutation targets and evaluate our approach in 125 classes of 5 large open source popular projects used in prior work. Our approach correctly discards mutations in 75.93% of the cases, and reduces the number of mutations by 71.38%.Conclusions: Our approach offers a good balance between the effort required to derive subsumption relations and the effectiveness for the targets considered in our evaluation in the context of strong mutation testing.