SAT-Based Synthesis of Fault-Tolerance

Ali Ebnenasir and Sandeep S. Kulkarni

Abstract

We present a technique where we use SAT solvers in automatic synthesis of fault-tolerant distributed programs from their fault-intolerant version. Since adding fault-tolerance to distributed programs is NP-complete, we use state-of-the-art SAT solvers to benefit from efficient heuristics integrated in SAT solvers to deal with the exponential complexity of adding fault-tolerance. Also, such SAT-based technique has the potential to use multiple instances of SAT solvers simultaneously so that independent sub-problems can be solved in parallel during synthesis.

Paper:


Return to the publication list
Return to the Sandeep's home page