We introduce two abstract models for multithreaded programs based on dynamic networks of pushdown systems. We address the problem of symbolic reachability analysis for these models. More precisely, we consider the problem of computing effective representations of their reachability sets using finite-state automata. We show that, while forward reachability sets are not regular in general, backward reachability sets starting from regular sets of configurations are always regular. We provide algorithms for computing backward reachability sets using word/tree automata, and show how these algorithms can be applied for flow analysis of multithreaded programs. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Bouajjani, A., Müller-Olm, M., & Touili, T. (2005). Regular symbolic analysis of dynamic networks of pushdown systems. In Lecture Notes in Computer Science (Vol. 3653, pp. 473–487). Springer Verlag. https://doi.org/10.1007/11539452_36
Mendeley helps you to discover research relevant for your work.