跳到正文
研踪PaperTrail
← 研踪 PaperTrail

arXiv:2611.05668 · v1

Sundance: A Simple SMT Solver for Program Verification

Amar ShahBenjamin F. JonesCan CebeciJason Z. S. HuLee A. BarnettRémi DelmasMarijn HeuleBryan ParnoBruno Dutertre
cs.LO
首次提交 2026-11-04 05:56
版本更新 2026-11-04 05:56
雷达观测 2026-11-05 10:08
arXiv ↗PDF ↗

摘要

We present Sundance, an SMT solver for program verification written in about 13,600 lines of Rust. Sundance combines the Cadical SAT solver with congruence closure, linear arithmetic, algebraic datatypes, and pattern-based quantifier instantiation. Sundance produces eDRAT proofs for every unsat answer. On 21,531 queries from Verus, Dafny, and F*, Sundance is comparable to existing solvers, with 26--38 times fewer lines of code than Z3 and cvc5. We further show that its components can be swapped for Z3's arithmetic solver, MiniSat, and the Semper e-graph. We have open sourced Sundance.

查看 arXiv 原文 ↗阅读 PDF ↗

AI 论文解读

基于摘要 · 非全文审阅

此版本尚未生成 AI 解读。解读由后台任务生成并按论文版本保存，登录后共享已有结果。

版本差异

目前只观测到一个版本，无法比较变化。之后收录新版本时，会在这里对照标题、作者、分类和摘要。

观测到的版本

相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。

v1 · 2026-11-04 05:56 · 最新观测版本

Sundance: A Simple SMT Solver for Program Verification

We present Sundance, an SMT solver for program verification written in about 13,600 lines of Rust. Sundance combines the Cadical SAT solver with congruence closure, linear arithmetic, algebraic datatypes, and pattern-based quantifier instantiation. Sundance produces eDRAT proofs for every unsat answer. On 21,531 queries from Verus, Dafny, and F*, Sundance is comparable to existing solvers, with 26--38 times fewer lines of code than Z3 and cvc5. We further show that its components can be swapped for Z3's arithmetic solver, MiniSat, and the Semper e-graph. We have open sourced Sundance.

查看此版本解读 →查看此版本原文 ↗