Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10328876 | Electronic Notes in Theoretical Computer Science | 2005 | 26 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Ahmed Bouajjani, Javier Esparza, Tayssir Touili,