research
∙
06/08/2023
Partitioning Strategies for Distributed SMT Solving
For many users of Satisfiability Modulo Theories (SMT) solvers, the solv...
share
research
∙
05/17/2022
Reasoning About Vectors using an SMT Theory of Sequences
Dynamic arrays, also referred to as vectors, are fundamental data struct...
research
∙
07/28/2021
Satisfiability and Synthesis Modulo Oracles
In classic program synthesis algorithms, such as counterexample-guided i...
research
∙
05/28/2021
Fair and Adventurous Enumeration of Quantifier Instantiations
SMT solvers generally tackle quantifiers by instantiating their variable...
research
∙
05/07/2021
lazybvtoint at the SMT Competition 2020
lazybvtoint is a new prototype SMT-solver, that will participate in the ...
research
∙
04/23/2021
Politeness and Stable Infiniteness: Stronger Together
We make two contributions to the study of polite combination in satisfia...
research
∙
07/23/2019
CVC4SY for SyGuS-COMP 2019
CVC4Sy is a syntax-guided synthesis (SyGuS) solver based on bounded term...
research
∙
05/24/2019
Towards Bit-Width-Independent Proofs in SMT Solvers
Many SMT solvers implement efficient SAT-based procedures for solving fi...
research
∙
06/20/2018
CVC4 at the SMT Competition 2018
This paper is a description of the CVC4 SMT solver as entered into the 2...
research
∙
04/13/2018
On Solving Quantified Bit-Vectors using Invertibility Conditions
We present a novel approach for solving quantified bit-vector formulas i...
research
∙
11/29/2017