SAtRes    News    TACAS'26: Incremental Proof Checking & SMT At Scale

TACAS'26: Incremental Proof Checking & SMT At Scale

January 7, 2026

We are happy to announce that two of our works have been accepted for publication at the 2026 TACAS conference, which will take place April 11–16, 2026 in Turin, Italy.

The paper Real-time Proof Checking for Distributed Incremental SAT Solving is a joint work with Katalin Fazekas (TU Wien) and Mathias Fleury and Armin Biere (Univ. Freiburg) that renders distributed incremental SAT solving dependable and trustworthy. We devised a formal and practical framework based on the incremental proof logging format LIDRUP and our distributed real-time proof checking approach ImpCheck. The resulting proof checking approach offers great flexibility in that it supports dynamic re-scheduling of computational resources and allows to safely share clauses across workers that operate on deviating assumptions and formula increments. Experiments with our distributed solver MallobSat on up to 1216 cores show that this approach checks incremental SAT tasks with small overhead (about 33%) over unchecked solving.

The paper Massively Parallel Bit-precise Verification with Bitwuzla and Mallob is a joint work with Aina Niemetz and Mathias Preiner (Stanford Univ.). It presents the first massively parallel solver for SMT theories related to bit-precise verification that scales up to 768 cores. The system is based on a liaison of the sequential bit-blasting SMT solver Bitwuzla and our distributed automated reasoning platform Mallob. We particularly leveraged Mallob’s features of low-overhead distributed incremental SAT solving and flexible multi-tasking to provide an alternative, scalable SAT solving backend to Bitwuzla’s SAT-driven abstraction refinement procedure.