Jump to Content
Tim King

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.
Authored Publications
Google Publications
Other Publications
Sort By
  • Title
  • Title, descending
  • Year
  • Year, descending
    FUDGE: Fuzz Driver Generation at Scale
    Yaohui Chen
    Markus Kusano
    Caroline Lemieux
    Wei Wang
    Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ACM
    Preview abstract At Google we have found tens of thousands of security and robustness bugs by fuzzing C and C++ libraries. To fuzz a library, a fuzzer requires a fuzz driver—which exercises some library code—to which it can pass inputs. Unfortunately, writing fuzz drivers remains a primarily manual exercise, a major hindrance to the widespread adoption of fuzzing. In this paper, we address this major hindrance by introducing the Fudge system for automated fuzz driver generation. Fudge automatically generates fuzz driver candidates for libraries based on existing client code. We have used Fudge to generate thousands of new drivers for a wide variety of libraries. Each generated driver includes a synthesized C/C++ program and a corresponding build script, and is automatically analyzed for quality. Developers have integrated over 200 of these generated drivers into continuous fuzzing services and have committed to address reported security bugs. Further, several of these fuzz drivers have been upstreamed to open source projects and integrated into the OSS-Fuzz fuzzing infrastructure. Running these fuzz drivers has resulted in over 150 bug fixes, including the elimination of numerous exploitable security vulnerabilities. View details
    Deciding Local Theory Extensions via E-matching
    Kshitij Bansal
    Andrew Reynolds
    Clark Barrett
    Thomas Wies
    Computer Aided Verification, Springer (2015), pp. 87-105
    A Concurrency Problem with Exponential DPLL(T) Proofs
    Liana Hadarean
    Alex Horn
    SMT (2015)
    Practical SMT-based type error localization
    Zvonimir Pavlinovic
    Thomas Wies
    ICFP, ACM (2015), pp. 412-423
    A tour of CVC4: How it works, and how to use it
    Morgan Deters
    Andrew Reynolds
    Clark Barrett
    Cesare Tinelli
    FMCAD, IEEE (2014), pp. 7
    Finding minimum type error sources
    Zvonimir Pavlinovic
    Thomas Wies
    OOPSLA, ACM (2014), pp. 525-542
    Leveraging linear and mixed integer programming for SMT
    Clark Barrett
    Cesare Tinelli
    FMCAD, IEEE (2014), pp. 139-146
    Simplex with sum of infeasibilities for SMT
    Clark Barrett
    Bruno Dutertre
    FMCAD, IEEE (2013), pp. 189-196
    Exploring and categorizing error spaces using BMC and SMT
    Clark Barrett
    SMT (2011)
    CVC4
    Clark Barrett
    Christopher L. Conway
    Morgan Deters
    Liana Hadarean
    Dejan Jovanovic
    Andrew Reynolds
    Cesare Tinelli
    Computer Aided Verification, Springer (2011), pp. 171-177