SMT Theory Arbitrage: Approximating Unbounded Constraints Using Bounded Theories

Explore a groundbreaking approach to improving SMT solver performance in this 19-minute video presentation from PLDI 2024. Delve into the concept of "theory arbitrage," which transforms unbounded constraints into bounded ones, potentially speeding up constraint solving by orders of magnitude. Learn how this novel method, implemented in the STAUB tool, applies abstract interpretation to infer bounds and create underapproximations of unbounded problems. Discover the significant performance improvements achieved across nonlinear integer benchmarks and how this technique enables the use of compiler optimization-based methods like SLOT for unbounded SMT theories. Gain insights into the practical applications of this approach, including its integration into a termination proving tool resulting in a 9% overall performance boost. Access supplementary materials and explore the potential of this innovative technique to expand the set of tractable problems in program analysis and beyond.