Trace-Based Temporal Verification for Message-Passing Programs

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.