使用黑盒变异模糊测试检测 SMT 求解器中的严重错误
软件工程
2020-04-14 v1
摘要
形式化方法广泛使用 SMT 求解器来判断公式可满足性，例如在软件验证、系统性测试生成和程序合成中。然而，由于其复杂实现，求解器可能包含导致不正确结果的严重错误。鉴于求解器在软件可靠性中的广泛适用性，依赖此类不正确结果可能产生有害后果。本文提出 STORM，一种用于检测 SMT 求解器中严重错误的新型黑盒变异模糊测试技术。我们在七个成熟求解器上运行该模糊器，发现了 29 个先前未知的严重错误。STORM 已在流行求解器部署前的新特性测试中得到使用。
引用
@article{arxiv.2004.05934,
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},
journal= {arXiv preprint arXiv:2004.05934},
year = {2020}
}