Program analysis as model checking of abstract interpretations

Abstract

This paper presents a collection of techniques, a methodology, in which abstract interpretation, flow analysis, and model checking are employed in the representation, abstraction, and analysis of programs. The methodology shows the areas of intersection of the dierent techniques as well as the opportunites that exist when one technique is used in support of another. The methodology is presented as a three-step process: First, from a (small-step) operational semantics deffnition and a program, one constructs a program model, which is a state-transition system that encodes the program's executions. Second, abstraction upon the program model is performed, reducing the detail of information in the model's nodes and arcs. Finally, the program model is analyzed for properties of its states and paths. © 1998 Springer-Verlag Berlin Heidelberg.