Flow logics for constraint based analysis

Abstract. Flow logic offers a compact and versatile notation for ex-pressing the acceptability ofsolutions to program analysis problems. In contrast to previous logical formulations of program analysis it aims at integrating existing approaches to data flow analysis and control flow analysis. It is able to deal with a broad variety of language paradigms, program properties, kinds of formal semantics, and methods u ed for computing the best solution. In this paper we illustrate how a compositional flow logic (in "succinct" form) can be systematically transformed into an efficient exhaustive pro-cedure for computing hebest solution of a set of constraints generated. This involves transformations to attribute grammars and to specifica-tions of the ("verbose") form used in control flow analysis