English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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 theToolBus 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.

A prototype implementation of a distributed Satisfiability Modulo Theories solver in the ToolBus framework