A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework

David DéharbeSilvio RaniseJorgiano Vidal

An increasing number of verification tools (e.g., softwaremodel-checkers) require the use of SatisfiabilityModulo Theories (SMT) solvers to implement the backendsfor the automatic analysis of specifications andproperties. The most prominent approach to build SMTsolvers consists in integrating an efficient Boolean solverwith decision procedures capable of checking the satisfiabilityof sets of ground literals in selected theories. Althoughthe problem of checking the satisfiability of arbitraryBoolean combinations of atoms modulo a backgroundtheory is NP-hard, there is a strong demand forhigh-performance SMT-solvers.In this paper, we describe the design and prototype implementation of-to the best of our knowledge-the firstdistributed SMT solver. The emphasis is on providingways to reduce the implementation effort and to make thesystem easily extensible. This is achieved in two ways: (a)we re-use as much as possible the code of an availablesequential SMT solver and (b) we adopt the TOOLBUSarchitecture for rapid prototyping. The behavior of thedistributed SMT solver was tested on a set of problemswhich are representative of those generated by softwareverification techniques. The experiments show the possibilityto obtain super-linear speed-ups of the distributedSMT solver with respect to its sequential version.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: