Automata-theoretic techniques for the analysis of multithreaded programs

Ahmed Bouajjani
LIAFA, Université de Paris 7
Friday, 9 May, 2003 (All day)
NO

We consider the verification problem of programs with unbounded (1) recursive procedure calls, and (2) dynamic creation of concurrent processes. We show different models for programs based on extended automata and process rewrite systems, and show different approaches for tackling their verification problem.

In a first approach, programs are modeled using term rewrite systems called PRS (for process rewrite systems). These models are more powerful than pushdown automata 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 prefix rewrite system and a multiset rewrite system. We define a generic procedure which constructs a finite representation of the set of all reachable configurations of a given PRS, provided that its underlying multiset rewrite system is effectively semilinear (preserves semilinearity). We represent PRS reachability sets by means of a class of tree automata with unbounded width. Our procedure can be instantiated in different ways leading to various reachability analysis procedures for classes of PRSs.

In a second approach, programs are modeled using a more general class of rewrite systems (including concurrent pushdown systems). The reachability problem for this model is undecidable. Therefore, we propose a method for analyzing such models based on computing abstractions of their sets of computation paths for which emptiness can be decided. Our method allows to compute such abstractions as least solutions of a system of language constraints. Given a program, (1) we build a system of constraints which characterizes precisely the set of its computation paths, and then (2) this system can be solved in various abstract domains leading to abstract analysis with different precision and cost. We show how to construct this set of constraints using automata-theoretic techniques for reachability analysis of process rewrite systems, and how to solve this set of constraints in a framework based on abstract interpretation.