一句话：提出 STORM，一种黑盒变异模糊测试技术，用于发现 SMT 求解器中的关键缺陷。
形式化方法广泛使用 SMT 求解器判定公式可满足性，例如软件验证、系统化测试生成和程序合成。然而求解器实现复杂，可能包含导致不可靠结果的关键缺陷；依赖此类不可靠结果会带来严重后果。本文提出 STORM，一种新颖的黑盒变异模糊测试技术，用于检测 SMT 求解器中的关键缺陷。作者在七个成熟求解器上运行该模糊测试器，发现 29 个此前未知的关键缺陷。STORM 已被用于在部署前测试流行求解器的新特性。
Formal methods use SMT solvers extensively for deciding formula satisfiability, for instance, in software verification, systematic test generation, and program synthesis. However, due to their complex implementations, solvers may contain critical bugs that lead to unsound results. Given the wide applicability of solvers in software reliability, relying on such unsound results may have detrimental consequences. In this paper, we present STORM, a novel blackbox mutational fuzzing technique for detecting critical bugs in SMT solvers. We run our fuzzer on seven mature solvers and find 29 previously unknown critical bugs. STORM is already being used in testing new features of popular solvers before deployment.
@inproceedings{paperbot5811,
title = {Detecting critical bugs in SMT solvers using blackbox mutational fuzzing},
author = {Muhammad Numair Mansur and Maria Christakis and Valentin Wüstholz and Fuyuan Zhang},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3409763}
}