Abstract Interpretation Based Formal Methods and Future Challenges

Abstract Interpretation Based Formal Methods and Future Challenges Patrick Cousot École normale supérieure, Département d'informatique, 45 rue d'Ulm, 75230 Paris cedex 05, France Abstract. In order to contribute to the solution of the software reliabil? ity problem, tools have been designed to analyze statically the run-time behavior of programs. Because the correctness problem is undecidable, some form of approximation is needed. The purpose of abstract interpre? tation is to formalize this idea of approximation. We illustrate informally the application of abstraction to the semantics of programming languages as well as to static program analysis. The main point is that in order to reason or compute about a complex system, some information must be lost, that is the observation of executions must be either partial or at a high level of abstraction. A few challenges for static program analysis by abstract interpretation are finally briefly discussed. The electronic version of this paper includes a comparison with other formal methods: typing , model-checking and deductive methods. 1 Introductory Motivations The evolution of hardware by a factor of 106 over the past 25 years has lead to the explosion of the size of programs in similar proportions. The scope of application of very large programs (from 1 to 40 millions of lines) is likely to widen rapidly in the next decade. Such big programs will have to be designed at a reasonable cost and then modified and maintained during their lifetime (which is often over 20 years).

• trace semantics


• methods


• since program


• algorithms provide


• programs only


• since such


• programs


• only semi-algorithms


• such big programs