Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
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. In Proc. of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '03, 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:

@inproceedings{BET03,
    author = {A. Bouajjani and J. Esparza and T. Touili},
    booktitle = {Proc. of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '03},
    title = {A Generic Approach to the Static Analysis of Concurrent Programs with Procedures},
    year = {2003}
}

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