




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 SIGPLANSIGACT 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 contextfree languages, which is undecidable, can be reduced to them. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of contextfree languages. We consider two classes of abstractions: finitechain 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 SIGPLANSIGACT 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.  

