## 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.

Original language | English |
---|---|

Pages (from-to) | 62-73 |

Number of pages | 12 |

Journal | Conference Record of the Annual ACM Symposium on Principles of Programming Languages |

DOIs | |

State | Published - 2003 |

Externally published | Yes |

Event | The 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - New Orleans, LA, United States Duration: 15 Jan 2003 → 17 Jan 2003 |

## Keywords

- Abstraction
- Concurrent programs with procedures
- Kleene algebras
- Pushdown systems
- Static analysis
- Verification