Name
Abstract | ||
|---|---|---|
Verification of concurrent systems is difficult because of their inherent nondeterminism. Modern verification requires clean specifications of inter-thread interferences and modular reasoning over separated components. But for message-passing models, a general reasoning system, which meets these standards, is still in demand. Here we propose a new logic for verifying distributed programs modularly. We concretize the concept of event traces to represent interactions among distributed agents, and constrain the environmental interferences by logical invariants. The verification is compositional w.r.t. agents as long as some inter-agent constraints are satisfied. Using this logic we successfully verified two classic message-passing algorithms: leader election and merging network. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1109/TASE.2014.14 | TASE |
Keywords | Field | DocType |
leader election,concurrency control,message-passing programs,temporal reasoning,distributed program verification,merging network,trace-based temporal verification,concurrent system verification,temporal logic,message passing,modular reasoning,interthread interference specifications,program verification,formal specification,computational modeling,semantics,concurrent computing,cognition | Leader election,Functional verification,Programming language,Computer science,Intelligent verification,Runtime verification,Theoretical computer science,Concurrent computing,Reasoning system,High-level verification,Message passing,Distributed computing | Conference |
Citations | PageRank | References |
0 | 0.34 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jinjiang Lei | 1 | 0 | 0.34 |
| Zongyan Qiu | 2 | 436 | 41.04 |
| Zhong Shao | 3 | 897 | 68.80 |