Integrating Loop Acceleration into Bounded Model Checking

TL;DR

This paper tightly integrate acceleration techniques into SMT-based bounded model checking and uses so-called blocking clauses to prove safety of examples where BMC diverges, showing that this approach is highly competitive for proving unsafety, and orthogonal to existing techniques for proving safety.

Abstract

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.