Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems

Опубликовано 6 сентября 2016, 5:42

We introduce 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-based techniques. We show that, while forward reachability sets are not regular in general (but context-free), 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. This is a joint work with Markus Mueller-Olm and Tayssir Touili.