Precise Analysis of Large Industry Code

Static analysis of code is very effective in finding common programmer errors but it comes at a price - a large number of false positives. Model checking, on the other hand, is very precise but does not scale up. We have developed a tool that combines both techniques and also implements a novel loop abstraction. The tool was run on 2 million lines of embedded code to analyze for two properties - division by zero and array index out of bounds. In other experiments we compared the precision of our tool to that achieved by tools implementing abstract interpretation. This paper presents details of the tool and the results of evaluations that we have carried out to measure the scalability and to compare the precision of our method on industry code against other static analysis tools.