Abstract | ||
---|---|---|
Proofs of progress properties often require fairness assumptions Directly incorporating global fairness assumptions in a compositional method is difficult, given the local flavor of such reasoning We present a fully automated local reasoning algorithm which handles fairness assumptions through a process of iterative refinement Refinement strengthens local proofs by the addition of auxiliary shared variables which expose internal process state; it is needed as local reasoning is inherently incomplete Experiments demonstrate that the new algorithm shows significant improvement over standard model checking. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1007/978-3-642-14295-6_46 | CAV |
Keywords | Field | DocType |
local proof,compositional method,auxiliary shared variable,internal process state,compositional reasoning,local flavor,fairness assumption,new algorithm,global fairness assumption,local reasoning algorithm,local reasoning,standard model | Iterative refinement,Reasoning algorithm,Shared variables,Process state,Computer science,Algorithm,Theoretical computer science,Mathematical proof,Compositional reasoning,Dash | Conference |
Volume | ISSN | ISBN |
6174 | 0302-9743 | 3-642-14294-X |
Citations | PageRank | References |
7 | 0.59 | 27 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ariel Cohen | 1 | 86 | 5.63 |
Kedar S. Namjoshi | 2 | 948 | 50.41 |
Yaniv Sa'ar | 3 | 230 | 14.70 |