arXiv subjects

Bruno Dutertre

Publications and source records attributed to Bruno Dutertre.

3 recordsLinked to original sources

arXiv2026

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.

cs.LO↗

arXiv2021

Interpolation and Model Checking for Nonlinear Arithmetic

We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the model-constructing satisfiability (MCSAT) framework of SMT. We use it to develop an interpolation procedure for any MCSAT-supported theory. In particular, this method leads to an effective interpolation procedure for nonlinear real arithmetic. We evaluate the new procedure by integrating it into a model checker and comparing it with state-of-art model-checking tools for nonlinear arithmetic.

cs.LO↗

arXiv2020

Solving bitvectors with MCSAT: explanations from bits and pieces (long version)

We present a decision procedure for the theory of fixed-sized bitvectors in the MCSAT framework. MCSAT is an alternative to CDCL(T) for SMT solving and can be seen as an extension of CDCL to domains other than the Booleans. Our procedure uses BDDs to record and update the sets of feasible values of bitvector variables. For explaining conflicts and propagations, we develop specialized word-level interpolation for two common fragments of the theory. For full generality, explaining conflicts outside of the covered fragments resorts to local bitblasting. The approach is implemented in the Yices 2 SMT solver and we present experimental results.

cs.LO↗