Name
Abstract | ||
|---|---|---|
We combine a prior incomplete deadlock-freedom-checking approach with two new reachability techniques to create a more precise deadlock-freedom-checking framework for concurrent systems. The reachability techniques that we propose are based on the analysis of individual components of the system; we use static analysis to summarise the behaviour that might lead components to this system state, and we analyse this summary to assess whether components can cooperate to reach a given system state. We implement this new framework on a tool called DeadlOx. This implementation encodes the proposed deadlock-freedom analysis as a satisfiability problem that is later checker by a SAT solver. We demonstrate by a series of practical experiments that this tool is more accurate than (and as efficient as) similar incomplete techniques for deadlock-freedom analysis. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-48989-6_3 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Computer science,Static analysis,Boolean satisfiability problem,Deadlock,Reachability,Theoretical computer science | Conference | 9995 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.41 |
References | Authors | |
11 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pedro R. G. Antonino | 1 | 33 | 4.57 |
| Thomas Gibson-Robinson | 2 | 105 | 10.12 |
| A. W. Roscoe | 3 | 1436 | 247.82 |