Advertisement
Published in:
2005 | OriginalPaper | Chapter
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems
Authors : Ahmed Bouajjani, Markus Müller-Olm, Tayssir Touili
Published in: CONCUR 2005 – Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.