Program Analysis through Finite Tree Automata Helmut Seidl

Dynamic Pushdown Networks (dpn’s) have recently been introduced as a conve-nient abstraction of systems which provide recursive procedure calls and spawning of concurrent tasks such as Java programs [1, 4–6]. We show how the executions of dpn’s can naturally be represented through ranked trees. The configuration reached by a program execution then can be read off from the sequence of leaves of this execution tree. This observation allows us to reduce decision problems such as reachability of configurations within a regular set for dpn’s to standard decision problems for finite tree automata. Our reduction does not only shed fresh light onto dpn’s but also provides us with new efficient algorithms which can be implemented through standard libraries for finite tree automata. Finite tree automata on the other hand, can be nicely represented by specific Horn clauses. In the presentation, we therefore indicate how these algorithms can be realized by means of generic solvers for