SAtRes    News    ETAPS & TACAS Awards for Massively Parallel SMT Solving

ETAPS & TACAS Awards for Massively Parallel SMT Solving

April 20, 2026

Our TACAS'26 publication “Massively parallel bit-precise verification with Bitwuzla and Mallob” – joint work with Aina Niemetz and Mathias Preiner (Stanford University) - received three awards at the combined ETAPS conferences 2026. These include the ETAPS-wide Best Tool Paper Award and (independently) the TACAS Distinguished Artifact Award, in addition to one of ETAPS’ Distinguished Paper Awards.

ETAPS and TACAS 2026 award certificates for the “Bitwuzllob” paper

Our open-source tool Bitwuzllob constitutes an integration of the bit-blasting SMT solver Bitwuzla into the massively parallel automated reasoning platform Mallob. This liaison proves particularly useful because Bitwuzla reduces SMT problems to series of plain incremental SAT solving queries, which Mallob is uniquely equipped to process at parallel and distributed scales. The tool, which allows to solve bit-precise verification problems with hundreds of parallel cores, essentially combines the best of Bitwuzla and Mallob and “clearly improves the state of the art, outperforming prior SMT parallelization approaches and achieving unprecedented speedups” (ETAPS 2026 Best Tool Paper Award Committee).

Following this success, we are eager to continue our productive (and fun!) collaboration and aim to push efficient parallel and distributed SMT solving further.