Reproduce “Sundance: A Simple SMT Solver for Program Verification” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Amar Shah, Benjamin F. Jones, Can Cebeci, Jason Z. S. Hu, Lee A. Barnett, Rémi Delmas, Marijn Heule, Bryan Parno and 1 more
Sundance is a small SMT solver for formulas produced by program verifiers. It combines Boolean search with modular theory reasoning and emits an eDRAT proof for unsatisfiable answers. Written in 13,612 lines of Rust, it solves 90.2% of held-out Verus queries within 60 seconds, but only 91.3% of those queries fall within its supported theory fragment, and it trails proof-enabled Z3 and cvc5.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.