[pl-seminar] Reminder: Touili talk at 4:00, Cookies NOW

[Jonathon Giffin <giffin@xxxxxxxxxxx>]

4:00 pm, 1325 CS (Cookies: 3:30 pm, 2310 CS)
Programming  Languages  Seminar:  Tayssir  Touili,  Carnegie Mellon University,

   "Reachability Analysis of Process Rewrite Systems:  Applications to the Ver-
   ification of Multithreaded Recursive Programs"

   We  consider  the verification problem of programs with unbounded (1) recur-
   sive procedure calls, and (2) dynamic creation of concurrent processes. Pro-
   grams 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 pro-
   grams without process creation, and multi-threaded programs  without  recur-
   sive  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 sev-
   eral 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.

   (This is a joint work with Ahmed Bouajjani)