Identifying method-level mutation subsumption relations using Z3

doi:10.1016/j.infsof.2020.106496

Identifying method-level mutation subsumption relations using Z3

2021-04-01

14

PRE

AI

Márcio Niemeyer Martins de Queiroz Guimarães

DOI：10.1016/j.infsof.2020.106496

原文链接

原文求助

摘要

En 中文

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.

Keyword:

Mutation analysis

Redundant mutants

Theorem proving

Identifying method-level mutation subsumption relations using Z3

摘要

AI总结

期刊

机构