Many concurrent and distributed systems are safety-critical and therefore have to provide a high degree of assurance. Important properties of such systems are frequently proved on the specification level, but implementations typically deviate from specifications for practical reasons. Machine-checked proofs of bisimilarity statements are often useful for guaranteeing that properties of specifications carry over to implementations. In this paper, we present a way of conducting such proofs with a focus on network communication. The proofs resulting from our approach are not just machine-checked but also intelligible for humans.

翻译：许多并发与分布式系统具有安全关键性，因此必须提供高度的可靠性保障。此类系统的重要性质通常在规格层面得以证明，但实际实现的系统常因实践原因偏离规格。双模拟关系语句的机器验证证明，对于确保规格的性质能够迁移至实现系统往往具有重要价值。本文提出了一种聚焦网络通信的证明方法。采用该方法得出的证明不仅通过了机器验证，而且对人类而言清晰可读。