A prototype implementation of a distributed satisfiability modulo theories solver in the ToolBus framework
AUTOR(ES)
Déharbe, David, Ranise, Silvio, Vidal, Jorgiano
FONTE
Journal of the Brazilian Computer Society
DATA DE PUBLICAÇÃO
2008-03
RESUMO
An increasing number of verification tools (e.g., software model-checkers) require the use of Satisfiability Modulo Theories (SMT) solvers to implement the back-ends for the automatic analysis of specifications and properties. The most prominent approach to build SMT solvers consists in integrating an efficient Boolean solver with decision procedures capable of checking the satisfiability of sets of ground literals in selected theories. Although the problem of checking the satisfiability of arbitrary Boolean combinations of atoms modulo a background theory is NP-hard, there is a strong demand for high-performance SMT-solvers. In this paper, we describe the design and prototype implementation of-to the best of our knowledge-the first distributed SMT solver. The emphasis is on providing ways to reduce the implementation effort and to make the system easily extensible. This is achieved in two ways: (a) we re-use as much as possible the code of an available sequential SMT solver and (b) we adopt the TOOLBUS architecture for rapid prototyping. The behavior of the distributed SMT solver was tested on a set of problems which are representative of those generated by software verification techniques. The experiments show the possibility to obtain super-linear speed-ups of the distributed SMT solver with respect to its sequential version.
Documentos Relacionados
- Optimization of reinforced concrete beams using Solver tool
- A runtime stability analysis of clock synchronization precision on a time-triggered bus prototype
- A Framework supporting collaboration on the distributed design of integrated systems
- Iron-Sulfur Flavoprotein (Isf) from Methanosarcina thermophila Is the Prototype of a Widely Distributed Family
- Servidor web distribuído com diferenciação de serviços - implementação e avaliação de um protótipo