Write a Blog >>

Loops with high or arbitrary bounds are very common in programs, it is useful to verify assertions in them, and Bounded Model Checkers (BMCs) will often struggle with those loops, taking a very long time or never terminating. In this paper, we propose a novel technique that can significantly expedite verification for such loops. The key insight of our technique is that Inner portions of such programs are often sufficient to prove those assertions. Our tool, Qicc, uses our technique and is able to quickly perform verification on C programs with manageable overhead. We demonstrate this by comparing the performance of Qicc to a state-of-the-art bounded model checker.