Thu Aug 26, 11-12, 4549 Boelter Hall

Reachability analysis of Process Rewrite Systems: 
Application to the verification of multithreaded recursive programs

Tayssir Touili
CMU

We consider the verification problem of programs with unbounded
(1) recursive procedure calls, and (2) dynamic creation of concurrent
processes. Programs are modeled using term rewrite systems called PRS (for
process rewrite systems). These models are more powerful than pushdown
systems and Petri nets, two common models for reasoning about, respectively,
recursive programs without process creation, and multi-threaded programs
without recursive calls. A PRS can actually be seen as the nesting of a
pushdown system and a Petri net.

We develop automata techniques allowing to build finite representations of
the forward/backward sets of reachable configurations of PRSs modulo various
term structural equivalences (corresponding to properties of the operators
of sequential composition and parallel composition).
We show that, in several cases, these reachability sets can be represented
by polynomial size finite bottom-up tree-automata.
When associativity and commutativity of the parallel composition is taken
into account, nonregular representations based on (a decidable class of)
counter tree automata are sometimes needed.

Joint work with Ahmed Bouajjani.

Host: Jens Palsberg