Centre de Recherche en Informatique- Ecole des Mines de Paris

Abstract — Software validation and verification are critical for almost systems whose failure is unacceptable. This is a very expensive process, typically costing 50 % of the total software development costs. We show in this paper how program analyses can be used automatically to perform efficient and effective verifications, e.g array bound checking and uninitialized variable checking. These verifications are based on array regions, the analyses that collect information about the way array elements used and defined by programs. With useful knowledge of the program properties provided by these static analyses, the amount of additional code necessary to instrument the application is reduced to a minimum. Run-time checks are generated only when we do not know how to prove that they are useless. Dynamic errors that may cause potentially failure are caught and their consequences can be reduced by exception handling. Information provided by our analyses is helpful for the debugging process of large scale programs. All verifications are implemented in PIPS, the research compiler developed at École des Mines de Paris. Qualitative and quantitative experiments have done with industrial applications up to hundreds of thousand lines of code