|
SAT and Model Checking |
||||
|
|
Welcome to the Parallel SAT reachability page in DSL. Here you will have a chance to get acquainted with our on-going research in parallel SAT, All-SAT and Model Checking.
The SAT problem is the first NPC problem, and has been widely investigated along the years. Software tools for solving this problem were developed, which employ many heuristics, and are capable of solving problems with millions of variables.
One of the industrial uses for these tools is in Bounded Model Checking (BMC), where the transition relation of a model, along with a property which has to hold, are converted into a CNF formula, which is then solved in a SAT solver.
Another important problem of Model checking is the Reachability problem, where all the reachable states of a model are being searched for. One of the methods to solve this problem is by using an All-SAT solver to enumerate all the successors of a set of states. This procedure is called Image Computation, and repeating it yields all the reachable stated of the model.
In our research we are developing a distributed platform for solving the Reachability problem, using a novel All-SAT solver we developed.
|
|
||
|
|
||||
