Tim King

I joined Google in September 2015 where I am currently a Software Engineer. The topic I am the most passionate about is satisfiability modulo theories (SMT). The SMT problem is determining the satisfiability of first-order formulas modulo background theories and is often done with respect to a specific syntactic fragment, such as quantifier free formulas or linear arithmetic terms. SMT is closely related to propositional satisfiability. Some of my other areas of interest include automated test case generation, automated reasoning, symbolic execution, type inference, verification, dynamic program analysis, and optimization. I received a BS with Honors in Computer Science from Stanford University in 2008. After this, I worked with Clark Barrett on my Ph.D. at New York University until 2014. My Ph.D. thesis is titled “Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic.” During my Ph.D., I interned at a number of laboratories including Bell Labs, SRI International, and MIT Lincoln Labs. Before joining Google, I was a post-doctoral researcher at Verimag working with David Monniaux. I am one of the authors of the state-of-the-art Satisfiability Modulo Theories solver CVC4, and I am actively involved in its maintenance. I am the author of its decision procedures for linear real and integer arithmetic. In the yearly International Satisfiability Modulo Theories Competition, CVC4 won the category of quantifier free linear real arithmetic in 2012, 2014, 2015 and 2016 and won the category of quantifier free linear integer arithmetic in 2016. I chaired the 14th International Workshop on Satisfiability Modulo Theories (SMT 2016).

Previous Publications

  •   

    A Concurrency Problem with Exponential DPLL(T) Proofs

    Liana Hadarean, Alex Horn, Tim King

    SMT (2015)

  •   

    Deciding Local Theory Extensions via E-matching

    Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, Thomas Wies

    Computer Aided Verification, Springer (2015), pp. 87-105

  •  

    Practical SMT-based type error localization

    Zvonimir Pavlinovic, Tim King, Thomas Wies

    ICFP, ACM (2015), pp. 412-423

  •   

    A tour of CVC4: How it works, and how to use it

    Morgan Deters, Andrew Reynolds, Tim King, Clark Barrett, Cesare Tinelli

    FMCAD, IEEE (2014), pp. 7

  •   

    Finding minimum type error sources

    Zvonimir Pavlinovic, Tim King, Thomas Wies

    OOPSLA, ACM (2014), pp. 525-542

  •   

    Leveraging linear and mixed integer programming for SMT

    Tim King, Clark Barrett, Cesare Tinelli

    FMCAD, IEEE (2014), pp. 139-146

  •   

    Simplex with sum of infeasibilities for SMT

    Tim King, Clark Barrett, Bruno Dutertre

    FMCAD, IEEE (2013), pp. 189-196

  •   

    CVC4

    Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli

    Computer Aided Verification, Springer (2011), pp. 171-177

  •  

    Exploring and categorizing error spaces using BMC and SMT

    Tim King, Clark Barrett

    SMT (2011)