Publications (8)
Anomalous Recurrence Properties of Markov Chains on Manifolds of Negative Curvature
John Armstrong, Tim King
We present a recurrence-transience classification for discrete-time Markov chains on manifolds with negative curvature. Our classification depends only on geometric quantities asso…
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…
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…
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…
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…
Curved Schemes for SDEs on Manifolds
John Armstrong, Tim King
Given a stochastic differential equation (SDE) in whose solution is constrained to lie in some manifold , we propose a class of numerical sch…