Authors
Abstract
Verification of concurrent systems is difficult because of the inherent nondeterminism. Modern verification requires better locality and modularity. Reasoning of shared memory systems has gained much progress in these aspects. However, modular verification of distributed systems is still in demand. In this paper, we propose a new reasoning system for message-passing programs. It is a novel logic that supports Hoare style triples to specify and verify distributed programs modularly. We concretize the concept of event traces to represent interactions among distributed agents, and specify behaviors of agents by their local traces with regard to environmental assumptions. Based on trace semantics, the verification is compositional in both temporal and spatial dimensions. As an example, we show how to modularly verify an implementation of merging network.
Published
In Proc. the 11th International Colloquium on Theoretical Aspects of Computing (ICTAC' 2014), Bucharest, Romania, Sept., 2014. © 2014 Springer-Verlag.
Conference Version [PDF]
Technical Report [PDF]