Structural operational semantics as a basis for static program analysis
Daniel Le Métayer, David Maria Schmidt · ACM Computing Surveys · 1996
interpretation was defined originally in terms of flow-charts or dynamic discrete systems [3]. From the usual flow-chart operational semantics, a socalled static (or collecting) semantics is derived automatically by attaching to each program point (flow-chart arc) the set of contexts (states) that flow to that point during execution. The collecting semantics summarizes "what really happens at run-time," and the goal of an abstract semantics is to compute properties for the program points that describe the concrete context sets. The abstract semantics does so by executing the flowchart with abstract values that represent context properties. The above formulation is simple and effective, but flow-charts suffer major weaknesses which preclude their use as a general framework for static program analysis: they are too low-level and they do not enjoy the compositionality property. A subsequent advance was the formulation of abstract interpretation in a compositional manner via denotational s...