Message Chains for Distributed System Verification

Explore a 17-minute conference talk from OOPSLA2 2023 that introduces an innovative approach to verifying asynchronous distributed programs. Discover how the proposed automated bookkeeping method based on message chains can simplify the verification process by revealing structure in distributed system executions. Learn about the development of a verification prototype for the P programming language that integrates message chains, and its application to 16 benchmarks from related work, a new benchmark, and two industrial benchmarks. Gain insights into how message chains can simplify existing proofs and provide comparable runtime performance to existing methods. Delve into the extension of this work to support specification mining, and understand how message chains offer sufficient structure for existing learning and program synthesis tools to automatically infer meaningful specifications using only execution examples.