1 citations · 1 across the 1 of their papers we have counts for
2 papers
cs.LO2021
Interpolation and Model Checking for Nonlinear Arithmetic
Dejan Jovanović, Bruno Dutertre
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…
cs.LO2020★ 1 cited
Solving bitvectors with MCSAT: explanations from bits and pieces (long version)
Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre
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…