Can Cebeci, Nikolaj Bjørner, George Candea, Clément Pit-Claudel
SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously quickly produced proof to fail or time out. This paper addresses a common cause of outcome instability (i.e., unsat/unknown fluctuations) in the context of program verification. We demonstrate that the generation (i.e., depth) accounting used to make quantifier instantiation practical and implemented in multiple state-of-the-art SMT solvers is non-confluent (i.e., prone to divergence), and that this leads to instability. We then address this deficiency and develop a new accounting method that is stable. The new method is justified using a sequence of refinements from an abstract, confluent solver model all the way to our implementation in Z3. Our empirical evaluation demonstrates that our implementation reduces outcome instability by 94% in the unstable core of the Mariposa benchmark without leading to performance regressions.
Amar Shah, Benjamin F. Jones, Can Cebeci, Jason Z. S. Hu, Lee A. Barnett, Rémi Delmas, Marijn Heule, Bryan Parno 等 9 位作者
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.