Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems
复制标题
DOI：
10.1007/11539452_36
复制
发表时间：
2005-08
期刊：
影响因子：
--
通讯作者：
A. Bouajjani;M. Müller-Olm;Tayssir Touili
中科院分区：
文献类型：
--
作者：
A. Bouajjani;M. Müller-Olm;Tayssir Touili
我们介绍了两个基于下推系统动态网络的多线程程序抽象模型，并解决了这些模型的符号可达性分析问题。更确切地说，我们认为使用有限状态自动机计算其可达集的有效表示的问题。我们表明，虽然前向可达性集是不定期的一般情况下，向后可达性集从定期的配置集总是定期的。我们提供的算法计算向后可达集使用字/树自动机，并显示这些算法可以应用于多线程程序的流分析。
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.