Thomas Gorges

Fully automatic source code analysis tools based on ab-stract interpretation have become an integral part of the embedded software development process in many compa-nies. And although these tools are of great help in identi-fying residual errors, they still possess a major drawback: analyzing industrial code comes at the cost of many spu-rious errors that must be investigated manually. The need for efficient development cycles prohibits extensive manual reviews, however. To overcome this problem, the combina-tion 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 auto-motive industry written in C, and show that the number of spurious errors emitted by an abstract interpretation prod-uct can be reduced considerably.