scholarly journals Reachability Analysis of Asynchronous Dynamic Pushdown Networks Based on Tree Semantics Approach

2018 ◽  
Vol 4 (4) ◽  
pp. 287
Author(s):  
Guodong Wu ◽  
Junyan Qian
Keyword(s):  
Reachability Analysis ◽  
Concurrent Programs ◽  
Abstract Model ◽  
Reachability Problem ◽  
Interleaving Semantics ◽  
Recursive Procedures ◽  
Backward Analysis

<em>ADPN (Asynchronous Dynamic Pushdown Networks) are an abstract model for concurrent programs with recursive procedures and dynamic thread creation. Usually, asynchronous dynamic pushdown networks are described with interleaving semantics, in which the backward analysis is not effective. In order to improve interleaving semantics, tree semantics approach was introduced. This paper extends the tree semantics to ADPN. Because the reachability problem of ADPN is also undecidable, we address the context-bounded reachability problem and provide an algorithm for backward reachability analysis with tree-based semantics Approach.</em>

On the State Reachability Problem for Concurrent Programs Under Power

2021 ◽  
pp. 47-59
Author(s):  
Parosh Aziz Abdulla ◽  
Mohamed Faouzi Atig ◽  
Ahmed Bouajjani ◽  
Egor Derevenetc ◽  
Carl Leonardsson ◽  
...  
Keyword(s):  
The State ◽  
Concurrent Programs ◽  
Reachability Problem

CONTROLLABILITY AND COOPERATIVENESS ANALYSIS FOR AUTOMATIC ABSTRACTION REFINEMENT

2006 ◽  
Vol 17 (04) ◽  
pp. 763-774
Author(s):  
FREDDY Y. C. MANG ◽  
PEI-HSIN HO
Keyword(s):  
Real World ◽  
Reachability Analysis ◽  
Experimental Results ◽  
The Other ◽  
Formal Property ◽  
Abstract Model ◽  
Abstraction Refinement ◽  
Automatic Abstraction ◽  
Property Verification ◽  
Refinement Algorithm

We present a new abstraction refinement algorithm to better refine the abstract model for formal property verification. In previous work, refinements are selected either based on a set of counter examples of the current abstract model, as in [5, 6, 7, 8, 9, 20, 21], or independent of any counter examples, as in [18]. We (1) introduce a new controllability analysis that is independent of any particular counter examples, (2) apply a new cooperativeness analysis that extracts information from a particular set of counter examples and (3) combine both to better refine the abstract model. We implemented the algorithm and applied it to verify several real-world designs and properties. We compared the algorithm against the abstraction refinement algorithms in [20] and [21] and the interpolation-based reachability analysis in [15]. The experimental results indicate that the new algorithm outperforms the other three algorithms in terms of runtime, abstraction efficiency (as defined in [20]) and the number of proven properties.

scholarly journals Graph models for reachability analysis of concurrent programs

1995 ◽  
Vol 4 (2) ◽  
pp. 171-213 ◽  
Author(s):  
Mauro Pezzè ◽  
Richard N. Taylor ◽  
Michal Young
Keyword(s):  
Reachability Analysis ◽  
Concurrent Programs ◽  
Graph Models
Sign in / Sign up

Export Citation Format

Share Document