ABSTRACT. The last years have brought substantial advancements to parallel and distributed SAT solving, including distributed clause-sharing solving that scales to thousands of cores, distributed incremental SAT solving, scalable proof production, and flexible multi-tasking of many (incremental) SAT tasks. This talk discusses to which degree SMT solving can profit from this technology. I touch on prior works on parallel and distributed SMT solving, outline our recent work on massively parallel bit-precise verification (combining the sequential bit-blasting SMT solver Bitwuzla with the distributed SAT platform Mallob), and discuss potential future directions for parallelizing general SMT solving.

ABSTRACT. Parallel approaches to SMT solving are an appealing avenue for improving SMT performance, especially with the increased availability of high-performance computing and cloud computing resources. One such approach is partitioning, a divide-and-conquer technique which endeavors to break the problem down into easier subproblems which can be solved in parallel. Unfortunately, this vision has been challenging to realize in practice. Specific challenges include the difficulty of finding good partitioning formulas, the inability to share information among subproblems, and the instability problem in SMT, all of which can contribute to some subproblems requiring even more time than the original problem. In this paper, we present fixed first decisions, a new technique which addresses the latter two challenges: it enables sharing of information among different partitions, and it enables a collaborative partitioning mode which mitigates the impact of difficult subproblems. We implement our approach using SMT-D and cvc5 and evaluate the implementation on SMT-LIB benchmarks, showing that it demonstrates a significant speedup over prior partitioning approaches.

ABSTRACT. The theory of arrays with select and store plays an important role in software verification and is therefore supported by virtually all state-of-the-art SMT solvers. There are many extensions, for instance by constant arrays, element-wise function applications, counting, or projections, that have been shown to preserve decidability. In recent work, a theory of arrays extended by constant arrays and sum predicates, called summation array logic (SAL), has been introduced and proven to be decidable in non-deterministic polynomial time. In SAL, it is possible to state assertions about the sum of all entries in a (finite or infinite) array of integers. This paper provides an eager approach to the satisfiability problem in SAL. The approach transforms a SAL formula to an equi-satisfiable formula in the theory of extensional arrays (extended with constant array operator), which can then be decided by an off-the-shelf SMT solver. The transformation produces a formula at most quadratic in the size of the input formula. Since there are no standard array benchmarks with sum constraints yet, the paper presents a new set of such benchmarks obtained by mutating existing SMT-LIB array benchmarks. The experiments show that the transformation-based decision procedure incurs only a relatively small overhead in terms of solving time.

ABSTRACT. Locality properties enable hierarchic and incremental satisfiability checking in theory extensions. In the context of Satisfiability Modulo Theories (SMT), locality reasoning provides an attractive way to obtain satisfiability procedures for various extensions of the theory of equality, including theories specifying data structures. We establish locality properties of expressive array theories that incorporate universal quantifiers and cardinality constraints.

ABSTRACT. Many verification tasks in computing require precise, unbounded relational reasoning. The cvc5 SMT solver provides some support for such tasks in the form of a relational solver that can automatically determine the satisfiability of sets of constraints over a simple set of relational operators. However, the current solver is quite limited in its ability to reason about more complicated concepts, such as transitive closure and cyclicity. In this paper, we propose extending the cvc5 relational solver with native support for reasoning about relational cyclicity. We propose two new predicates, acyclic and minimal, and we argue that these extensions will enable cvc5 to tackle more challenging tasks, such as reasoning about microarchitectural memory consistency models.

ABSTRACT. We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describe a Galois connection between sets of decidable theories, which picks out the largest set of decidable theories that can be combined with a given set of decidable theories. Using this, we exactly characterize the sets of decidable theories that can be combined with those satisfying well-known theory combination properties. This strengthens previous results and answers in the negative several long-standing open questions about the possibility of improving existing theory combination methods to apply to larger sets of theories. Additionally, the Galois connection gives rise to a complete lattice of theory combination properties, which allows one to generate new theory combination methods by taking meets and joins of elements of this lattice. We provide examples of this process, introducing new combination theorems. We situate both new and old combination methods within this lattice. This paper was originally presented at POPL 2026.