## Abstract

We present a generic approach for the analysis of concurrent programs with (unbounded) dynamic creation of threads and recursive procedure calls. We define a model for such programs based on a set of term rewrite rules where terms represent control configurations. The reachability problem for this model is undecidable. Therefore, we propose a method for analyzing such models based on computing abstractions of their sets of computation paths. Our approach allows to compute such abstractions as least solutions of a system of (path language) constraints. More precisely, given a program and two regular sets of configurations (process terms) T and T′, we provide (1) a construction of a system of constraints which characterizes the set of computation paths leading from T to T′, and (2) a generic framework, based on abstract interpretation, allowing to solve this system in various abstract domains leading to abstract analysis with different precision and cost.

Originalsprache | Englisch |
---|---|

Seiten (von - bis) | 153-178 |

Seitenumfang | 26 |

Fachzeitschrift | Electronic Notes in Theoretical Computer Science |

Jahrgang | 138 |

Ausgabenummer | 3 |

DOIs | |

Publikationsstatus | Veröffentlicht - 28 Dez. 2005 |

Extern publiziert | Ja |

Veranstaltung | Proceedings of the 6th International Workshop on Verification of Infinite-State Systems (INFINITY 2004) - Dauer: 4 Sept. 2004 → 4 Sept. 2004 |