Google Research

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).

Learn more about how we do research

We maintain a portfolio of research projects, providing individuals and teams the freedom to emphasize specific types of work