Abstract
Dynamic Pushdown Networks (dpn’s) have recently been introduced as a convenient 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.
Chapter PDF
Similar content being viewed by others
References
Bouajjani, A., Müller-Olm, M., Touili, T.: Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005, vol. 3653, pp. 473–487. Springer, Heidelberg (2005)
Nielson, F., Nielson, H.R., Seidl, H.: Normalizable Horn Clauses, Strongly Recognizable Relations and Spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002, vol. 2477, pp. 20–35. Springer, Heidelberg (2002)
Goubault-Larrecq, J.: Deciding \(\mathcal{\MakeUppercase{H}}_1\) by Resolution. Information Processing Letters 95(3), 401–408 (2005)
Lammich, P., Müller-Olm, M.: Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 287–302. Springer, Heidelberg (2007)
Lammich, P., Müller-Olm, M.: Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. P. Lammich, M. Müller-Olm, vol. 5079, pp. 205–220. Springer, Heidelberg (2008)
Lammich, P., Müller-Olm, M., Wenner, A.: Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. In: Int. Conf. on Computer-Aided Verification (CAV). LNCS. Springer, Heidelberg (to appear, 2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Seidl, H. (2009). Program Analysis through Finite Tree Automata. In: Maneth, S. (eds) Implementation and Application of Automata. CIAA 2009. Lecture Notes in Computer Science, vol 5642. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02979-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-02979-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02978-3
Online ISBN: 978-3-642-02979-0
eBook Packages: Computer ScienceComputer Science (R0)