A Reconstruction of Verification Techniques by Abstract Interpretation

Interpretation Giorgio Levi and Paolo Volpe Dipartimento di Informatica, Universit`a di Pisa Corso Italia 40, 56125 Pisa, Italy e-mail: flevi, volpepg@di.unipi.it 1 Introduction In this paper we study the application of abstract interpretation to the design of methods for verifying properties of programs. We obtain as a result a reconstruction of verification methods used in the field of logic programming and define a new framework to address the problem of verification. This application of abstract interpretation should not come as a surprise. A specification is simply a set of intended properties of a program. Thus it can naturally be viewed as an abstraction of the semantics of the program. Abstract interpretation allows us to make explicit the relations among semantics at different levels of abstraction through a lattice of abstractions. As already advocated by Cousot [CC92, Cou], this can be very helpful to understand, organize and synthesize proof methods for program verifica..