The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

Skip to content



Automata-based techniques for the analysis of dynamic concurrent programs

Bouajjani, A (Paris)
Tuesday 23 May 2006, 11:00-12:00

Seminar Room 1, Newton Institute


We propose formal models for dynamic programs with procedure calls and dynamic creation of concurrent processes. The considered models are based on (combinations of) various classes of rewrite systems such as multiset rewrite systems and prefix rewrite systems. We address the reachability analysis problem for such models. More precisely, we consider the problem of of computing finite representations of the (potentially infinite) sets of reachable configurations in such models. We consider finite word/tree automata for the representation of these reachability sets. The proposed constructions can be used for solving model-checking problems for the considered classes of infinite-state models.

Back to top ∧