Analysis of Message Passing Programs Using SMT-Solvers
AbstractWe consider message passing programs where processes communicate asynchronously over unbounded channels. The reachability problem for such systems are either undecidable or have very high complexity. In order to achieve efficiency, we consider the phase-bounded reachability problem, where each process is allowed to perform a bounded number of phases during a run of the system. In a given phase, the process is allowed to perform send or receive transitions (but not both). We present a uniform framework where the channels are assigned different types of semantics such as lossy, stuttering, or unordered. We show that the framework allows a uniform translation of bounded-phase reachability for each of the above mentioned semantics to the satisfiability of quantifierfree Presburger formulas. This means that we can use the full power of modern smt-solvers for efficient analysis of our systems. Furthermore, we show that the translation implies that bounded-phase reachability is np-complete. Finally, we prove that the problem becomes undecidable if we allow perfect channels or push-down processes communicating through (stuttering) lossy channels. We report on the result of applying the prototype on a number of non-trivial examples.