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.