2005 | OriginalPaper | Buchkapitel
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems
verfasst von : Ahmed Bouajjani, Markus Müller-Olm, Tayssir Touili
Erschienen in: CONCUR 2005 – Concurrency Theory
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.