一句话：提出 TestMC 框架，用差分/蜕变测试与有界穷举输入生成测试模型计数器，发现三个工具缺陷。
模型计数求有界公式解数，但现代计数器算法与启发式复杂，难以保证实现正确。本文是经验论文，提出 TestMC 框架，结合差分测试、蜕变测试、有界穷举输入生成与输入最小化来测试工业级模型计数器。作者用真实软件设计公式、TestMC 生成的小公式穷举集、CNF fuzzer 生成公式三类测试套件，测试 projMC、dSharp、Ganak、ApproxMC 四个工具。结果在三个工具中发现缺陷，导致崩溃、段错误、错误计数和资源耗尽；其中两个经报告后修复，第三个被认为无需修复。
Model counting is the problem for finding the number of solutions to a formula over a bounded universe. This is a classic problem in computer science that has seen many recent advances in techniques and tools that tackle it. These advances have led to applications of model counting in many domains, e.g., quantitative program analysis, reliability, and security. Given the sheer complexity of the underlying problem, today's model counters employ sophisticated algorithms and heuristics, which result in complex tools that must be heavily optimized. Therefore, establishing the correctness of implementations of model counters necessitates rigorous testing. This experience paper presents an empirical study on testing industrial strength model counters by applying the principles of differential and metamorphic testing together with bounded exhaustive input generation and input minimization. We embody these principles in the TestMC framework, and apply it to test four model counters, including three state-of-the-art model counters from three different classes. Specifically, we test the exact model counters projMC and dSharp, the probabilistic exact model counter Ganak, and the probabilistic approximate model counter ApproxMC. As subjects, we use three complementary test suites of input formulas. One suite consists of larger formulas that are derived from a wide range of real-world software design problems. The second suite consists of a bounded exhaustive set of small formulas that TestMC generated. The third suite consists of formulas generated using an off-the-shelf CNF fuzzer. TestMC found bugs in three of the four subject model counters. The bugs led to crashes, segmentation faults, incorrect model counts, and resource exhaustion by the solvers. Two of the tools were corrected subsequent to the bug reports we submitted based on our study, whereas the bugs we reported in the third tool were deemed by the tool authors to not require a fix.
DOI 原文 ·
@inproceedings{paperbot5963,
title = {TestMC},
author = {Muhammad Usman and Wenxi Wang and Sarfraz Khurshid},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3416563}
}