ISSN:
1573-0557
Keywords:
abstract interpretation
;
operational semantics
;
collecting semantics
;
simulation
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract We present trace-based abstract interpretation, a unification of severallines of research on applying Cousot-Cousot-style abstract interpretation a.i. tooperational 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. Aprogram‘s trace-based a.i. is also a computation tree whose nodes contain abstractions ofstate 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 collectingsemantics and state-based from path-based collecting semantics. We also expose therelationship between collecting semantics extraction and results garnered from flow-analytic and model-checking-based analysis techniques. We adapt concepts fromconcurrency 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 andcoinduction in response; small-step semantics generate sequences of programconfigurations 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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1007734417713
