Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob
Abstract
We present a distributed platform for massively parallel SMT solving that supports various theories for bit-precise reasoning, with and without quantifiers and push-pop incrementality. Our system is based on an integration of the state-of-the-art SMT solver Bitwuzla into the distributed job scheduling and automated reasoning platform Mallob, which allows Bitwuzla to make heavy use of Mallob ’s distributed incremental SAT solving engine. Our experimental evaluation shows that this approach outperforms prior SMT parallelization approaches and achieves unprecedented speedups at up to 768 cores.
Fields of Study & Subjects
Embedded Systems Design Techniques
Formal Methods in Verification
Parallel Computing and Optimization Techniques
Publication details
- Journal / source
- Lecture notes in computer science
- Publisher
- Springer Nature Switzerland
- Pages
- 170–191
- Publication date
- 1 January 2026
- Language
- EN