23 citations · 32 across the 5 of their papers we have counts for
5 papers
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…
A Decision Procedure for Separation Logic in SMT
Andrew Reynolds, Radu Iosif, Tim King
This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic ($\seplog$) interpreted over heaplets with data elements ranging over…
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic
Andrew Reynolds, Tim King, Viktor Kuncak
This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, impl…
On Deciding Local Theory Extensions via E-matching
Kshitij Bansal, Andrew Reynolds, Tim King +2
Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories of data types that commonly occur in software. This makes them important tools for automat…
A Concurrency Problem with Exponential DPLL(T) Proofs
Liana Hadarean, Alex Horn, Tim King
Many satisfiability modulo theories solvers implement a variant of the DPLL(T ) framework which separates theory-specific reasoning from reasoning on the propositional abstraction…