Psym: Efficient Symbolic Exploration of Distributed Systems

Lauren Pick, Ankush Desai, Aarti Gupta

Research output: Contribution to journalArticlepeer-review


Verification of distributed systems using systematic exploration is daunting because of the many possible interleavings of messages and failures. When faced with this scalability challenge, existing approaches have traditionally mitigated state space explosion by avoiding exploration of redundant states (e.g., via state hashing) and redundant interleavings of transitions (e.g., via partial-order reductions). In this paper, we present an efficient symbolic exploration method that not only avoids redundancies in states and interleavings, but additionally avoids redundant computations that are performed during updates to states on transitions. Our symbolic explorer leverages a novel, fine-grained, canonical representation of distributed system configurations (states) to identify opportunities for avoiding such redundancies on-The-fly. The explorer also includes an interface that is compatible with abstractions for state-space reduction and with partial-order and other reductions for avoiding redundant interleavings.

Original languageEnglish (US)
Pages (from-to)660-685
Number of pages26
JournalProceedings of the ACM on Programming Languages
StatePublished - Jun 6 2023

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality


  • binary decision diagrams
  • distributed systems
  • systematic exploration


Dive into the research topics of 'Psym: Efficient Symbolic Exploration of Distributed Systems'. Together they form a unique fingerprint.

Cite this