Helmut Seidl and Christian Fecht. Interprocedural Analysis Based on PDAs. , volume 97-06 of Forschungsbericht, 1997. Universität Trier, Mathematik/Informatik.

We present a unifying framework for the abstract interpretation of both imperative and logic languages. Our framework is based on a small-step operational semantics. Both the concrete and the abstract operational semantics are formalized by means of (input-free) pushdown automata. Starting from this abstract operational semantics, we systematically explore the design space of possible analyses. We introduce relational analysis both with forward and with backward (intraprocedural) accumulation and the corresponding functional analyses and clarify their relationships. Especially, we exhibit places where information is lost. We argue that the two analysis problems of (demand-driven) derivability and reachability can be jointly dealt with by local solvers. Finally, our approach allows to prove new and very general interprocedural coincidence theorems not only for imperative languages but also for Prolog. Thus, we are especially able to derive coincidence for groundness analysis with POS.

Reference: Bibtex