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

Ahmed Bouajjani, Javier Esparza, Tayssir Touili

Research output: Contribution to journalArticlepeer-review

33 Scopus citations


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 languages. We consider two classes of abstractions: finite-chain abstractions, which are abstractions whose domains do not contain 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.

Original languageEnglish
Pages (from-to)551-582
Number of pages32
JournalInternational Journal of Foundations of Computer Science
Issue number4
StatePublished - 2003
Externally publishedYes


  • Concurrent programs with procedures
  • Kleene algebras
  • abstraction
  • pushdown systems
  • static analysis
  • verification


Dive into the research topics of 'A generic approach to the static analysis of concurrent programs with procedures'. Together they form a unique fingerprint.

Cite this