Tim King

Tim's research focuses on satisfiability modulo theories, automated reasoning, testing, symbolic execution, type inference, verification, optimization, and applied formal methods in general. He received a BS with Honors in Computer from Stanford University in 2008 and a Ph.D. in Computer Science from New York University in 2014. Tim is an author of the Satisfiability Modulo Theories solver CVC4.

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)