Sciweavers

CONCUR
2005
Springer

Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems

14 years 4 months ago
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems
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.
Ahmed Bouajjani, Markus Müller-Olm, Tayssir T
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CONCUR
Authors Ahmed Bouajjani, Markus Müller-Olm, Tayssir Touili
Comments (0)