Infinitary control flow analysis

Defining the collecting semantics is usually the first crucial step in adapting the general methodology of abstract interpretation to the semantic framework or programming language at hand. In this paper we show how to define a collecting semantics for control flow analysis: due to the generality of the formulation we need to appeal to coinduction (or greatest fixed points) in order to define the analysis. We then prove the semantic soundness of the collecting semantics and that all totally deterministic instantiations have a least solution; this incorporates k-CFA, polymorphic splitting and a new class of uniform-k-CFA analyses.