Verification of parallel and recursive programs

Tayssir Touili, LIAFA


We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known  that typical dataflow problems for this model are undecidable, because the emptiness problem for the intersection of context-free languages, which is undecidable, can be reduced to them. We propose an algebraic framework for defining upper approximations of context-free languages. The approximations belong to different classes of commutative languages, i.e. languages that contain a word if and only if they contain all its permutations.

We show how to compute such approximations by combining automata theoretic techniques with algorithms for solving systems of polynomial inequations in commutative Kleene algebras.