I will join Columbia University as a tenure-track Assistant Professor in Jan. 2018. I obtained my Ph.D. degree in Computer Science from Yale University in 2016 and obtained my B.S. in Computer Science from Tsinghua University in 2011.

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.

[CV.pdf] [ResearchStatement.pdf]


  • Aug. 2011 to Aug. 2016, Yale University, Ph.D. in Computer Science.
    • 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)

Selected Conference Publications

Professional Experience

Yale University

    Research Assistant, Associate Research Scientist (Aug. 2011 - present)

    Working on CertiKOS , an extensible architecture for building certified OS kernels. As the lead developer of the project, verified a series of sequential and concurrent OS kernels in Coq with my Yale colleagues. The most realistic one is written in 6,500 lines of C and x86 assembly and runs on stock x86 multicore machines.

Tsinghua University

    Research Assistant (Spring 2011)

    Working on verifying the preemptive scheduling and nested interrupt handling of uC/OS-II running on the PowerPC platform. I presented this work as my undergraduate honors thesis.

Selected Talks

Building Fully Trustworthy OS Kernels through Formal Verification.
  • Aug. 2017, University of Washinton, WA.
  • Apr. 2017, Chicago Universit, IL.
  • Mar. 2017, University of Minnesota Twin Cities, MN.
  • Mar. 2017, Pennsylvania State University, PA.
  • Mar. 2017, New York University, NY.
  • Mar. 2017, Boston University, MA.
  • Feb. 2017, University of Connecticut, CT.
  • Feb. 2017, Columbia University, NY.
An Extensible Architecture for Building Certified Concurrent OS Kernels.
  • Dec. 2016, University of California, Davis, CA.
  • Dec. 2016, Columbia University, NY.
  • Nov. 2016, University of Pennsylvania, PA.
  • Nov. 2016, Princeton University, NJ.
  • Nov. 2016, OSDI, GA.
Deep Specifications and Certified Abstraction Layers.

Selected Awards

  • Dec. 2016, Distinction Dissertation, Yale University.
  • Aug. 2016, Nomination for ACM Dissertation Award, Yale University.
  • Feb. 2016, Robert Willets Carle Scholarship, Yale University.
  • Jan. 2015, Travel Grant for POPL15, NSF.
  • Aug. 2011, Doctoral Fellowship, Yale University.
  • Jul. 2011, Excellent Undergraduate (top 1.9%), Tsinghua University.
  • Jul. 2011, Excellent Undergraduate of Beijing City, China.
  • Jul. 2011, Hornors Undergraduate Thesis Award, Tsinghua University.
  • Oct. 2010, Sohu Scholarship, Tsinghua University.
  • Oct. 2009, Ticket Master Scholarship, Tsinghua University.
  • Oct. 2006, First Prize of National Mathematical Olympiad Competition, China.
  • Oct. 2006, First Prize of National Chemistry Olympiad Competition, China.

Teacing Experience

  • CPSC 458/558 Automatic Decision Systems (Fall 2015).
  • CPSC 422/522 Operating System Design and Implementation (Fall 2015).
  • CPSC 439/539 Software Engineering (Spring 2015 and Spring 2014).
  • CPSC 424/524 Parallel Programming Techniques (Fall 2014 and Fall 2013).
  • CPSC 439/539 Software Engineering (Spring 2015 and Spring 2014).
  • CPSC 112 Introduction to Programming Languages (Spring 2013 and Fall 2012).



Email: firstname dot lastname at yale dot edu

Office: AKW 303, Yale University

CertiKOS Layers

Layout based on BASIC by Download Website Templates