Integrated and Automated Abstract Interpretation, Verification and Testing of C/C++ Modules

Abstract. Starting from the perspective of safety-critical systems de-velopment in avionics, railways and the automotive domain, we advocate an integrated verification approach for C/C++ modules combining ab-stract interpretation, formal verification and conventional testing. It is interpretation results and, vice versa, how test automation techniques may help to reduce the well known problem of false alarms frequently encountered in abstract interpretations. As a consequence, verification tools integrating these different methodologies can provide a wider va-riety of useful results to their users and facilitate the bug localisation processes involved. When applied to C/C++ software, the problems of aliasing, type casts and mixed arithmetic and bit operations have to be handled on the level of constraint generation. We cope with this problem by using a symbolic interpretation method operating on an abstracted memory model. We describe the available tool support developed by the author, his research group and industrial partners