一句话：提出用弱变异测试与 Z3 证明方法级变异算子间的包含关系，以消冗余变异并降低变异分析成本。
变异分析成本高昂，识别冗余变异是降低成本的重要方向。论文提出通过证明方法级变异算子之间的包含关系来发现冗余变异，并基于弱变异测试构建可在 Z3 中编码的包含关系理论，覆盖 40 种变异目标（表达式或语句变异）。随后用 Z3 定理证明器证明若干包含关系，从而减少变异目标中的变异数量。作者将 MuJava 与包含部分包含关系的 MuJava-M 应用于 17 个项目共 187 个类。结果表明，该方法在 74.97% 的情况下能正确丢弃变异，并将变异数量减少 72.52%。
One recent promising direction in reducing costs of mutation analysis is to identify redundant mutations. We propose a technique to discover redundant mutations by proving subsumption relations among method-level mutation operators using weak mutation testing. We conceive and encode a theory of subsumption relations in Z3 for 40 mutation targets (mutations of an expression or statement). Then we prove a number of subsumption relations using the Z3 theorem prover, and reduce the number of mutations in a number of mutation targets. MuJava-M includes some subsumption relations in MuJava. We apply MuJava and MuJava-M to 187 classes of 17 projects. Our approach correctly discards mutations in 74.97% of the cases, and reduces the number of mutations by 72.52%.
DOI 原文 ·
@inproceedings{paperbot5923,
title = {Identifying mutation subsumption relations},
author = {Beatriz Souza},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3418921}
}