I obtained my Ph.D. degree in FLINT Group at the Department of Computer Science of Yale University . I received my B.S. in Computer Science in 2011 from Tsinghua University at Beijing, China.

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. [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.
    • 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 Experience

Yale University

    Research Associate (Aug. 2016 - present)

    Research Assistant (Aug. 2011 - Aug. 2016)

    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 Associate (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

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

  • 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: ronghui.gu at yale.edu

Office: AKW 305

             Yale University

Layout based on BASIC by Download Website Templates