4 citations · 4 across the 1 of their papers we have counts for
5 papers · 1 filter
Bitwuzla at the SMT-COMP 2020
Aina Niemetz, Mathias Preiner
In this paper, we present Bitwuzla, our Satisfiability Modulo Theories (SMT) solver for the theories of bit-vectors, floating-points, arrays and uninterpreted functions and their c…
DRAT-based Bit-Vector Proofs in CVC4
Alex Ozdemir, Aina Niemetz, Mathias Preiner +2
Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is transla…
Towards Bit-Width-Independent Proofs in SMT Solvers
Aina Niemetz, Mathias Preiner, Andrew Reynolds +3
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, however, cannot be used directly to reason about bit-vectors…
CVC4 at the SMT Competition 2018
Clark Barrett, Haniel Barbosa, Martin Brain +8
This paper is a description of the CVC4 SMT solver as entered into the 2018 SMT Competition. We only list important differences from the 2017 SMT Competition version of CVC4. For f…
On Solving Quantified Bit-Vectors using Invertibility Conditions
Aina Niemetz, Mathias Preiner, Andrew Reynolds +2
We present a novel approach for solving quantified bit-vector formulas in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We deri…