Integrating Loop Acceleration into Bounded Model Checking

arXiv (Cornell University)

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.

Authors 2

1. Florian Frohn Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

2. Jürgen Giesl Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany