Exploring The Relationship Between Unwind Bound and Model Checking Complexity in CBMC

Abstract

The C Bounded Model Checker (CBMC) is a widely used formal verification tool that operates directly on ANSI-C source code by bit-blasting straight-line programs into Boolean satisfiability (SAT) instances. While CBMC mitigates infinite state spaces by restricting loop iterations and recursion depths via a user-defined unwind bound ($k$) , the exact empirical relationship between this parameter and back-end solver complexity remains largely uncharacterized in existing literature. This paper systematically evaluates the impact of the maximum unwind depth on model checking complexity across three distinct software domains: array bounds, floating-point arithmetic, and heap manipulation. Utilizing metrics of execution runtime, memory footprint, and propositional variable/clause counts, we expose divergent complexity scaling behaviors. Our empirical results demonstrate that while simple non-looping floating-point operations scale under near-constant complexity , nested loops (e.g., Bubble Sort) incur a sharp quadratic complexity expansion ($O(k^2)$). Crucially, heap-intensive algorithms (e.g., In-Place Merge Sort and Singly-to-Doubly Linked List transformations) exhibit severe exponential state-space explosion, triggering solver timeouts at high unwinding thresholds. These findings challenge the intuition that model checking complexity mirrors a program's algorithmic time complexity , highlighting instead that structural loop layouts and memory-aliasing relationships dictate verification feasibility. Based on these insights, we provide concrete recommendations for iterative $k$-value scaling strategies to optimize bounded verification workflows.