Automated formal analysis methods such as program verification and synthesis algorithms often suffer from time
complexity of their decision procedures and also high space complexity known as the \emph{state explosion problem}. Symbolic
techniques, in which elements of a problem are represented by Boolean formulae, are desirable in the sense that they often remedy
the state explosion problem and time complexity of decision
procedures. Although symbolic techniques have successfully been used in program verification, their benefits have not yet been exploited
in the context of program synthesis and transformation extensively. In this paper, we present a symbolic method for automatic synthesis
of fault-tolerant distributed programs. Our experimental results on synthesis of classical fault-tolerant distributed problems such as
Byzantine agreement and token ring show a significant performance improvement by several orders of magnitude in both time and space
complexity. To the best of our knowledge, this is the first illustration where programs with large state space (beyond
$2^{100}$) is handled during synthesis.
Paper:
Return to the publication list
Return to the Sandeep's home page