CVC4. - Clark W. Barrett; Christopher L. Conway; Morgan Deters; Liana Hadarean; Dejan Jovanovic; Tim King 001; Andrew Reynolds 001; Cesare Tinelli (CAV, 2011)

Simplex with sum of infeasibilities for SMT. - Tim King 001; Clark W. Barrett; Bruno Dutertre (FMCAD, 2013)

A tour of CVC4: How it works, and how to use it. - Morgan Deters; Andrew Reynolds 001; Tim King 001; Clark W. Barrett; Cesare Tinelli (FMCAD, 2014)

Leveraging Linear and Mixed Integer Programming for SMT. - Tim King 001; Clark W. Barrett; Cesare Tinelli (SMT, 2014)

Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic. - Tim King 001 (2014)

Deciding Local Theory Extensions via E-matching. - Kshitij Bansal; Andrew Reynolds 001; Tim King 001; Clark W. Barrett; Thomas Wies (CAV (2), 2015)

Practical SMT-based type error localization. - Zvonimir Pavlinovic; Tim King 001; Thomas Wies (ICFP, 2015)

Finding Minimum Type Error Sources. - Zvonimir Pavlinovic; Tim King 001; Thomas Wies (Software Engineering & Management, 2015)

A Concurrency Problem with Exponential DPLL(T) Proofs. - Liana Hadarean; Alex Horn; Tim King 001 (CoRR, 2015)

An Instantiation-Based Approach for Solving Quantified Linear Arithmetic. - Andrew Reynolds 001; Tim King 001; Viktor Kuncak (CoRR, 2015)

A Decision Procedure for Separation Logic in SMT. - Andrew Reynolds 001; Radu Iosif; Cristina Serban; Tim King 001 (ATVA, 2016)

Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem. - Alexandre Maréchal; Alexis Fouilhé; Tim King 001; David Monniaux; Michaël Périn (VMCAI, 2016)

A Decision Procedure for Separation Logic in SMT. - Andrew Reynolds 001; Radu Iosif; Tim King 001 (CoRR, 2016)

Solving quantified linear arithmetic by counterexample-guided instantiation. - Andrew Reynolds 001; Tim King 001; Viktor Kuncak (Formal Methods Syst. Des., 2017)

CVC4 at the SMT Competition 2018. - Clark W. Barrett; Haniel Barbosa; Martin Brain; Duligur Ibeling; Tim King 001; Paul Meng; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli (CoRR, 2018)

FUDGE: fuzz driver generation at scale. - Domagoj Babic; Stefan Bucur; Yaohui Chen; Franjo Ivancic; Tim King 001; Markus Kusano; Caroline Lemieux; László Szekeres; Wei Wang (ESEC/SIGSOFT FSE, 2019)