News
FLoC'26: Mallob Tool Paper and a Natively Parallel Proof FrameworkFLoC'26: Mallob Tool Paper and a Natively Parallel Proof Framework
May 21, 2026
Illustration of our parallel proof checking approach for distributed clause-sharing SAT solving
We are happy to announce that two of our works have been accepted for publication at the 2026 Federated Logic Conferences (FLoC), which will take place in July in Lisbon, Portugal.
The CAV tool paper Mallob: Scalable Automated Reasoning On Demand (Dominik Schreiber, Niccolò Rigi-Luperti, Peter Sanders) presents our distributed Automated Reasoning platform Mallob to the wider verification community. We present the different capabilities and use cases of Mallob (such as incremental SAT for BMC, MaxSAT solving, and bit-blasting SMT solving), discuss a wide range of experimental results gathered throughout the last few years, and reflect on our system’s impact.
The SAT paper A Natively Parallel Proof Framework for Clause-Sharing SAT Solving (Ruben Götz, Michael Dörr, Dominik Schreiber) marks the first milestone in our DFG project Propositional Proofs as Big Data. We managed to devise a proof format for clause-sharing solving that allows to produce and check proofs in parallel. This greatly increases the scalability of fully dependable and certified SAT solving for critical use cases.