This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
27th International Conference on Distributed Computing Systems (ICDCS '07)
Exploiting Symbolic Techniques in Automated Synthesis of Distributed Programs with Large State Space
Toronto, Canada
June 25-June 27
ISBN: 0-7695-2837-3
Borzoo Bonakdarpour, Michigan State University
Sandeep S. Kulkarni, Michigan State University
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 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 2100) is handled during synthesis.
Citation:
Borzoo Bonakdarpour, Sandeep S. Kulkarni, "Exploiting Symbolic Techniques in Automated Synthesis of Distributed Programs with Large State Space," icdcs, pp.3, 27th International Conference on Distributed Computing Systems (ICDCS '07), 2007
Usage of this product signifies your acceptance of the Terms of Use.