4 citations · 8 across the 4 of their papers we have counts for
Showing 2019Show all
2 papers · 1 filter
cs.LO2019
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…
cs.LO2019
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…