A calculational approach to control-flow analysis by abstract interpretation. (English) Zbl 1149.68359

Alpuente, María (ed.) et al., Static analysis. 15th international symposium, SAS 2008, Valencia, Spain, July 16–18, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-69163-1/pbk). Lecture Notes in Computer Science 5079, 347-362 (2008).
Summary: We present a derivation of a control-flow analysis by abstract interpretation. Our starting point is a transition system semantics defined as an abstract machine for a small functional language in continuation-passing style. We obtain a Galois connection for abstracting the machine states by composing Galois connections, most notable an independent-attribute Galois connection on machine states and a Galois connection induced by a closure operator associated with a constituent-parts relation on environments. We calculate abstract transfer functions by applying the state abstraction to the collecting semantics, resulting in a novel characterization of demand-driven 0-CFA.
For the entire collection see [Zbl 1142.68002].


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI