Static Analysis versus Software Model Checking for Bug Finding

Static Analysis versus Software Model Checking for Bug Finding
复制标题

DOI:
10.1007/978-3-540-24622-0_17
复制
发表时间:
2004-01
期刊:
--
影响因子:
--
通讯作者:
D. Engler;M. Musuvathi
D. Engler;M. Musuvathi
中科院分区:
其他
文献类型:
--
作者:
D. Engler;M. Musuvathi

文献摘要

被引文献

相似文献

本文介绍了几年来使用静态分析来查找错误后进行软件模型检查的经验。我们最初认为两者之间的权衡是明确的:静态分析很容易,但主要会发现浅层错误,而模型检查需要更多工作,但严格来说会更好——它会发现更多错误,错误会更深,并且方法会更强大。这些期望常常是错误的。
This paper describes experiences with software model checking after several years of using static analysis to find errors. We initially thought that the trade-off between the two was clear: static analysis was easy but would mainly find shallow bugs, while model checking would require more work but would be strictly better – it would find more errors, the errors would be deeper, and the approach would be more powerful. These expectations were often wrong.