Skip to main content

Revising Distributed UNITY Programs is NP-Complete

Publication Type
Year of Publication
Conference/Journal Name
International Conference on Principles of Distributed Systems (OPODIS)
We focus on automated revision techniques for adding UNITY properties to distributed programs. We show that unlike centralized pro-
grams, where multiple safety properties along with one progress property can be simultaneously added in polynomial-time, addition of only one safety or one progress property to distributed programs is NP-complete. We also propose an efficient symbolic heuristic for adding a leads-to property to a distributed program. We demonstrate the application of this heuristic in automated synthesis of recovery paths in fault-tolerant distributed programs.