A generic approach to the static analysis of concurrent programs with procedures

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. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of context-free lanWe consider two classes of abstractions: finite-chain ions, which are abstractions whose domains do not any infinite chains, and commutative abstractions corresponding to classes of 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 Kleene algebras. Categories and Subject Descriptors

• Type: Conference
• Year: 2003
• Where: POPL
• Authors: Ahmed Bouajjani, Javier Esparza, Tayssir Touili
• Keywords: Automata Theoretic Techniques, POPL 2003, Programming Languages, Subject Descriptors, Typical Dataflow Problems