Abstract Interpretation in the Operational Semantics Hierarchy

Abstract

We systematically apply the principles of Cousot-Cousot-style abstract interpretation (a.i.) to the hierarchy of operational semantics definitions - flowchart, big-step, and small-step semantics. For each semantics format we examine the principles of safety and liveness interpretations, first-order and second-order analyses, and termination properties. Application of a.i. to data-flow analysis, model checking, closure analysis, and concurrency theory are demonstrated. Our primary contributions are separating the concerns of safety, termination, and efficiency of representation and showing how a.i. principles apply uniformly to the various levels of the operational semantics hierarchy and their applications.