I am an Assistant Professor of Computer Science at Columbia University.

My research interests span a range of areas in Programming Languages and Operating Systems, with a focus on language-based support for safety and security, certified system software, certified programming and compilation, formal methods, and concurrency reasoning.

I am also a co-founder of CertiK, a formal verification startup based on my research.

[CV.pdf] [ResearchStatement.pdf]


    My research group at Columbia University is looking for Ph.D./Master students, Postdocs, and Undergraduate interns. Check out our recent PLDI'18, OSDI'16, and POPL'15 CertiKOS papers (and the press release) for an overview of our latest breakthrough on building certified concurrent operating systems. If you know both systems and programming languages and are interested in building such bug-free and hacker-resistant systems, send me an email.


  • Aug. 2011 to Aug. 2016, Yale University, Ph.D. in Computer Science.
    • Advisor: Professor Zhong Shao
    • Thesis: An Extensible Architecture for Building Certified Sequential and Concurrent OS Kernels.
    • Distinction Dissertation of Yale Graduate School of Art and Science
    • Nomination for ACM Dissertation Award
  • Aug. 2007 to Jul. 2011, Tsinghua University, B.S. in Computer Science.
    • Rank: 4/118, GPA: 91.2/100
    • Excellent Undergraduate of Tsinghua University, top 1.9% (67 among 3543)
    • Honors Undergraduate Thesis of Tsinghua University, top 4% (5 among 118)

Professional Activities


Selected Awards



515 CSB, Columbia University


+1 (212) 939-7111

CertiKOS Layers (for fun)

Layout based on BASIC by Download Website Templates