Reachability Analysis of Synchronized PA Systems | Zendy

Ahmed Bouajjani | Zendy; Javier Esparza | Zendy; Tayssir Touili | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Reachability Analysis of Synchronized PA Systems

Author(s) -

Ahmed Bouajjani,

Javier Esparza,

Tayssir Touili

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.02.063

Subject(s) - reachability , undecidable problem , abstract interpretation , computer science , reachability problem , computation , set (abstract data type) , theoretical computer science , interpretation (philosophy) , model checking , static analysis , model of computation , path (computing) , process (computing) , decidability , programming language , algorithm

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research