Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems

August 19, 2005
Ahmed Bouajjani | Stanford University

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.

Speaker Details

Ahmed Bouajjani is a full Professor in Computer Science at the University Paris Diderot (Paris 7), and he is the head of the Verification group at Liafa (a joint laboratory of CNRS and the University of Paris 7). Previously, he was Associate Professor at the University Joseph Fourier (Grenoble) and a member of the Verimag laboratory. He was researcher on leave at CNRS in 1994-1996. He got his PhD and his “Habilitation” in Computer Science from the University Joseph Fourier (Grenoble). His research interests include: Formal modeling and verification methods, algorithmic verification of infinite-state systems, program verification, automata and logics. (URL: http://www.liafa.jussieu.fr/~abou)