I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - A Generic Approach to the Static Analysis of Concurrent Programs with Procedures

Reference:

A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. International Journal on Foundations of Computer Science, 14(4):551–582, 2003.

Abstract:

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.

Suggested BibTeX entry:

@article{IJFCS,
    author = {A. Bouajjani and J. Esparza and T. Touili},
    journal = {International Journal on Foundations of Computer Science},
    number = {4},
    pages = {551--582},
    title = {A Generic Approach to the Static Analysis of Concurrent Programs with Procedures},
    volume = {14},
    year = {2003}
}

GZipped PostScript (141 kB)
PDF (371 kB)
Conference version
January 2011: Michal Terepeta and Flemming Nielson have found a mistake in the paper: Lemma 1.2 does not hold as stated. We will try to repair it as soon as possible.