Psym: Efficient Symbolic Exploration of Distributed Systems
Explore an efficient symbolic exploration method for verifying distributed systems in this 18-minute conference talk from PLDI 2023. Learn about a novel approach that addresses scalability challenges by avoiding redundancies in states, interleavings, and computations during state updates. Discover how the presented tool, Psym, utilizes a fine-grained, canonical representation of distributed system configurations to identify and eliminate redundancies on-the-fly. Understand the tool's compatibility with state-space reduction abstractions and partial-order reductions. Examine empirical results demonstrating Psym's superior performance compared to existing exploration tools, its ability to verify common distributed protocols, and its scalability to real-world industrial case studies. Gain insights into the potential of this innovative approach for improving the verification process of complex distributed systems.