Polynomial Time Synthesis of Byzantine Agreement

We present a polynomial time algorithm for automatic synthesis of fault-tolerant distributed programs starting from fault-intolerant versions of those programs. Since this synthesis problem is known to be NP-hard, our algorithm relies on heuristics to reduce the complexity. We demonstrate that our algorithm suffices to synthesize an agreement program that tolerates a byzantine fault. Keywords: Fault-tolerance, Formal methods, Program synthesis, Program transformation, Distributed program