[ARTIFACT] Sundance: A Simple SMT Solver for Program Verification
This is the artifact for our TACAS '27 submission. Sundance is an SMT solver for program verification with support for uninterpreted functions, linear integer arithmetic, and quantifier instantiation. In this artifact we compare it against other SMT solvers like Z3, cvc5, and alt-ergo on program verification benchmarks from Verus, Dafny, and F*.
Authors
- Bruno Dutertre (ORCID: https://orcid.org/0000-0002-6284-380X)
- Lee A. Barnett (ORCID: https://orcid.org/0000-0003-1282-8596)
- Marijn J. H. Heule (ORCID: https://orcid.org/0000-0002-5587-8801)
- Jason Z. S. Hu (ORCID: https://orcid.org/0000-0001-6710-6262)
- Rémi Delmas (ORCID: https://orcid.org/0000-0002-1994-9094)
- Bryan Jeffery Parno (ORCID: https://orcid.org/0000-0002-9113-1684)
- Benjamin F. Jones (ORCID: https://orcid.org/0000-0001-9697-9388)
- Can Cebeci (ORCID: https://orcid.org/0009-0007-8923-2666)
- Amar Shah
Institutions
- Amazon (United States) (US)
- École Polytechnique Fédérale de Lausanne (CH)
- Carnegie Mellon University (US)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-10-28
- DOI
- https://doi.org/10.5281/zenodo.23740047
- Primary Topic
- Logic, programming, and type systems
- Type
- article
- Field-Weighted Citation Impact
- 0.00