Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. In more detail, we quantify the benefits of interval analysis on two benchmarks: the Intel Core Power Management firmware and 9537 programs in the ReachSafety category of the International Competition on Software Verification. Our results show that interval analysis is essential in solving 203 unique benchmarks.

翻译：有界模型检验（BMC）是一种广泛使用的软件验证技术。尽管该技术已取得诸多成功，但仍存在若干限制因素，从状态空间爆炸到完备性缺失等。多年来，区间分析被反复提出作为应对这些限制的部分解决方案。本研究评估了区间分析的计算成本是否能为BMC性能带来足够显著的改进，从而证明其应用价值。具体而言，我们通过两个基准测试量化区间分析的效益：英特尔酷睿电源管理固件，以及国际软件验证竞赛ReachSafety类别中的9537个程序。实验结果表明，区间分析对于解决203个独特基准测试具有关键作用。