Bounded Model Checking (BMC) is a powerful technique for proving unsafety. However, finding deep counterexamples that require a large bound is challenging for BMC. On the other hand, acceleration techniques compute "shortcuts" that "compress" many execution steps into a single one. In this paper, we tightly integrate acceleration techniques into SMT-based bounded model checking. By adding suitable "shortcuts" on the fly, our approach can quickly detect deep counterexamples. Moreover, using so-called blocking clauses, our approach can prove safety of examples where BMC diverges. An empirical comparison with other state-of-the-art techniques shows that our approach is highly competitive for proving unsafety, and orthogonal to existing techniques for proving safety.

翻译：有界模型检验（BMC）是一种证明系统不安全性的有效技术。然而，对于需要较大界限的深层反例，BMC 的检测面临挑战。另一方面，加速技术通过计算“捷径”，将多次执行步骤“压缩”为单一步骤。本文中，我们将加速技术与基于 SMT 的有界模型检验进行紧密集成。通过动态添加合适的“捷径”，我们的方法能够快速检测深层反例。此外，通过使用所谓的阻塞子句，我们的方法能够证明那些导致 BMC 发散的系统安全性。与其他前沿技术的实证比较表明，我们的方法在证明不安全性方面极具竞争力，且在证明安全性方面与现有技术形成互补。