Abstract

Characterizing the set of reachable states of a distributed protocol that uses asynchronous message-passing communication is difficult due to the exponential number of possible interleavings of local executions. Any syntactic expression overapproximating the set of reachable states is an invariant formula of the system, and is a valuable tool that can aid programmers in understanding global program behavior. In this paper, we propose a method for obtaining a formula that approximates the set of reachable states; we call this formula a likely invariant, and we learn it using information only obtained from system executions. Our method doubles up as a way for identifying states that may not be known to be reachable (based on the best-known likely invariant) and hence may appear anomalous to the system designer. In some cases, they may be actually anomalous and may indicate a lurking (heisenbug). Our method …

Date

January 20, 2025

Authors

Yuan Xia, Deepayan Sur, Aabha Shailesh Pingle, Jyotirmoy V Deshmukh, Mukund Raghothaman, Srivatsan Ravi

Book

International Conference on Verification, Model Checking, and Abstract Interpretation

Pages

3-25

Publisher

Springer Nature Switzerland