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

Author: Jan Peleska

Abstract:
Starting from the perspective of safety-critical systems development in avionics, railways and the automotive domain, we advocate an integrated verification approach for C/C++ modules combining abstract interpretation, formal verification and conventional testing. It is illustrated how testing and formal verification can benefit from abstract interpretation results and, vice versa, how test automation techniques may help to reduce the well known problem of {\em false alarms} frequently encountered in abstract interpretations. As a consequence, verification tools integrating these different methodologies can provide a wider variety 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.

PDF file (263KB)