Abstract Semantics for Alias Analysis in K

This paper presents an approach to integrating analysis and verification methods in the K framework. We adopt the abstract interpretation perspective where the concrete system to be analyzed/verified is mapped into a suitable abstract system, and collecting semantics is applied over the abstract system to obtain the analysis/verification method itself. As such, we present the K perspective of collecting semantics over K operational semantics for abstract systems. For a good degree of generality we consider that abstract systems are K specifications of (finite) pushdown systems. We give the collecting semantics as a generic set of K rules parametrized by the K specification of a finite pushdown system. Further, we describe a case study which instances collecting semantics with alias analysis. For this, the abstract system is defined as an imperative language which maintains enough pointer and flow information for alias analysis to be decidable. The K specification of this imperative language fits the frame of a finite pushdown system specification.