|
Abstract Interpretation in the Operational Semantics Hierarchy
David A. Schmidt March 1997 |
Abstract:We systematically apply the principles of Cousot-Cousot-style abstract interpretation 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. Applications of abstract interpretation 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 abstract interpretation principles apply uniformly to the various levels of the operational semantics hierarchy and their applications Available as PostScript, PDF, DVI. |