Using Model Checking Techniques for Symbolic Synthesis of Distributed Programs ∗

Given the non-determinism and race conditions in distributed programs, the ability to pro-vide assurance about them is crucial. Our work focuses on incremental synthesis where we modify existing (fault-intolerant) distributed programs to add fault-tolerance. We concentrate on reducing the complexity of such synthesis using techniques –symmetry and parallelism — from model checking. We apply these techniques in the context of deadlock resolution. In particular, incremental synthesis requires removal of certain program actions that could violate safety in the presence of faults and such removal may eliminate all outgoing transitions from some states rendering them to be deadlock states. We focus on reducing the complexity of resolving such deadlock states using symmetry and/or parallelism. We show that these approaches provide a significant speedup separately as well as together