research
∙
06/08/2023
Partitioning Strategies for Distributed SMT Solving
For many users of Satisfiability Modulo Theories (SMT) solvers, the solv...
share
research
∙
05/18/2022
Realizability Checking of Contracts with Kind 2
We present a new feature of the open-source model checker Kind 2 which c...
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
∙
05/13/2021
Merit and Blame Assignment with Kind 2
We introduce two new major features of the open-source model checker Kin...
research
∙
04/23/2021
Politeness and Stable Infiniteness: Stronger Together
We make two contributions to the study of polite combination in satisfia...
research
∙
07/02/2020
Smt-Switch: a solver-agnostic C++ API for SMT Solving
This extended abstract describes work in progress on Smt-Switch, an open...
research
∙
08/26/2019
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
This work is a part of an ongoing effort to prove the correctness of inv...
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