SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
summary
Transforms expensive unbounded integer and real constraints into bounded bitvector/fp versions by inferring per-constraint widths via abstract interpretation (choose minimal width that underapproximates the computation) and verifying results with a portfolio verification fallback running original solver in parallel. Implemented as STAUB, it solves thousands more timed-out cases, yields ≈1.4× average speedup on nonlinear integer benchmarks, unlocks up to 3× with SLOT optimizations, and produces a 9% end-to-end gain in a termination prover.
AI-written summary · about
chapters (9)
- 0:00SMT constraints motivation
- 1:44Theory Arbitrage concept
- 3:50Fixed bit-width limits
- 6:39Dynamic bit-width inference
- 9:47Verification for correctness
- 10:53Experimental results
- 13:00Impact and future directions
- 14:44STAB tool
- 15:04Q&A
related talks
13mProgram Analysis via Efficient Symbolic Abstraction
18mScalable Floating-Point Satisfiability via Staged Optimization
15mInter-theory Dependency Analysis for SMT String Solvers
30mBit-Precise Reasoning via Int-Blasting
13mInteractive Bit Vector Reasoning using Verified Bitblasting
20mOptimal Program Synthesis via Abstract Interpretation
01h 02mTheory and Control
35mThe Mastermind behind Refinement Types