Automatic predicate abstraction of C programs

Model checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of systems. Recently, there has been significant interest in applying model checking to software. For infinite-state systems like software, abstraction is even more critical. Techniques for abstracting software are a prerequisite to making software model checking a reality. We present the first algorithm to automatically construct a predicate abstraction of programs written in am industrial programming language such as C, and its implementation in a tool -- C2BP.…