Tim King

I joined Google in September 2015. Since 2018, I have led a small team working on static analysis for the Go programming language. Other work I have at Google includes FUDGE, a system for synthesizing C++ fuzz targets at scale, and fuzzing at scale infrastructure. My work has touched several other areas of programming languages, formal methods, and software security including: decision procedures, automated reasoning, symbolic execution, type inference, and formal verification.
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. Before Google, I have worked at several research laboratories including Verimag, Bell Labs, SRI International, and MIT Lincoln Labs.
I am one of the authors of the Satisfiability Modulo Theories solver CVC4. The SMT problem is determining the satisfiability of first-order formulas modulo background theories. I am the author of its decision procedures for linear real and integer arithmetic.