Reducing False Positives by Combining Abstract Interpretation and Bounded Model Checking

Fully automatic source code analysis tools based on abstract interpretation have become an integral part of the embedded software development process in many companies. And although these tools are of great help in identifying residual errors, they still possess a major drawback: analyzing industrial code comes at the cost of many spurious errors that must be investigated manually. The need for efficient development cycles prohibits extensive manual reviews, however. To overcome this problem, the combination of different software verification techniques has been suggested in the literature. Following this direction, we present a novel approach combining abstract interpretation and source code bounded model checking, where the model checker is used to reduce the number of false error reports. We apply our methodology to source code from the automotive industry written in C, and show that the number of spurious errors emitted by an abstract interpretation product can be reduced considerably.