LISP and Symbolic Computation, 10(3)237-271
Trace-Based Abstract Interpretation of Operational SemanticsDavid A. Schmidt, Kansas State University, Computing and Information Sciences Department, 234 Nichols Hall, Manhattan, KS 66506 USA
|
Abstract: We present trace-based abstract interpretation, a
unification of several lines of research on applying
Cousot-Cousot-style abstract interpretation a.i. to operational
semantics definitions (such as flowchart, big-step, and small-step
semantics) that express a program?s semantics as a concrete
computation tree of trace paths. A program?s trace-based a.i. is also
a computation tree whose nodes contain abstractions of state and whose
paths simulate the paths in the program's concrete computation
tree. Using such computation trees, we provide a simple explanation of
the central concept of collecting semantics, and we distinguish
concrete from abstract collecting semantics and state-based from
path-based collecting semantics. We also expose the relationship
between collecting semantics extraction and results garnered from
flow-analytic and model-checking-based analysis techniques. We adapt
concepts from concurrency theory to formalize "safe" and "live" a.i.'s
for computation trees; in particular, coinduction techniques help
extend fundamental results to infinite computation trees. Problems specific to the various operational semantics methodologies are discussed: Big-step semantics cannot express divergence, so we employ a mixture of induction and coinduction in response; small-step semantics generate sequences of program configurations unbounded in size, so we abstractly interpret source language syntax. Applications of trace-based a.i. to data-flow analysis, model checking, closure analysis, and concurrency theory are demonstrated. Keywords: abstract interpretation, operational semantics, collecting semantics, simulation |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)