Parallel SMT Solver
Rhishikesh Shrikant Limaye and Sanjit A. Seshia
Satisfiability Modulo Theories is the problem of checking satisfiability of a formula with respect to first-order theories, such as bit-vector arithmetic and arrays. It has applications in formal verification, program analysis, software test generation, and security. Over recent years, several solvers have improved in their capability to solve SMT problems, but the scale of problems created from real applications have also increased a great deal. With the advent of chip multiprocessor systems, it is natural to look for ways to parallelize the solving techniques to improve performance.
Our initial focus is on parallelizing the abstraction-refinement procedure used in UCLID to solve bit-vector formulas . It is currently a tight sequential procedure in which successive over-approximations and under-approximations are generated and are solved by a SAT solver. We are investigating ways to run multiple abstraction-refinement loops in parallel, and share information between them. Abstraction-refinement is a widely used technique in formal verification, so the lessons learned will also be useful in many other contexts.
- R. Bryant, D. Kroening, J. Ouaknine, S. Seshia, O. Strichman, and B. Brady, "Deciding Bit-Vector Arithmetic with Abstraction," Proceedings of TACAS 2007, LNCS 4424/2007, March 2007, pp. 358-372.