3 papers
cs.LO2018
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…
cs.LO2016
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…
cs.LO2015
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…