Bounded Model Checking (BMC) is a powerful technique for proving reachability of error states, i.e., 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" to the SMT-problem on the fly, our approach can quickly detect deep counterexamples, even when only using small bounds. 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的有界模型检测中。通过在SMT问题中动态添加适当的“捷径”，我们的方法能够快速检测到深层反例，即使仅使用小边界。此外，利用所谓阻塞子句，我们的方法可证明BMC发散的示例的安全性。与其它先进技术的实证比较表明，我们的方法在证明不安全性方面具有极强的竞争力，并且与现有的安全性证明技术正交。