Boolean and Cartesian Abstraction for Model Checking C Programs

The problem of model checking a specification in form of a C program with recursive procedures and many thousands of lines of code has not been addressed before. In this paper, we show how we attack this problem using an abstraction that is formalized with the Cartesian abstraction. It is implemented through a source-to-source transformation into a ‘Boolean’ C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice.