Ronghui Gu (顾荣辉)

Hiring!

My research group at Columbia University is looking for Ph.D./Master students, Postdocs, and Undergraduate interns. Check out our recent 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.

Professional Experience

Columbia University

Assistant Professor (2018 - present)

Yale University

Research Assistant, Associate Research Scientist (2011 - 2017)

Worked on CertiKOS, an extensible architecture for building certified OS kernels. As the key developer and author of the project, I 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)

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

Education

• 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)

Selected Conference Publications

• Certified Concurrent Abstraction Layers.

  (with Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjoberg, C. Hao, D. Constanzo, and T.Ramananandro)

  PLDI 2018 (To appear)

• An Auditing Language for Preventing Correlated Failures in the Cloud.

  (with with Ennan Zhai, Ruzica Piskac, Xun Lao, and Xi Wang)

  OOPSLA 2017 (Accept rate: 29%)

• CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.

  (with Z. Shao, C. Hao, X. Wu, J. Kim, V. Sjoberg, and D. Constanzo)

  OSDI 2016 (Accept rate: 18%)

  Media coverage: Yale News, International Business Times, Yale Daily News

  Honor: Selected in the Research Highlights section of the CACM.

• End-to-End Verification of Information-Flow Security for C and Assembly Programs.

  (with D. Constanzo and Z. Shao)

  PLDI 2016 (Accept rate: 16%)

• Toward Compositional Verification of Interruptible OS Kernels and Device Drivers.

  (with C. Hao, X. Wu, Z. Shao, and J. Lockerman)

  PLDI 2016 (Accept rate: 16%)

• Deep specifications and Certified Abstraction Layers.

  (with J. Koenig, T. Ramananandro, Z. Shao, X. Wu, S. Weng, H. Zhang, and Y. Guo)

  POPL 2015 (Accept rate: 23%)

Professional Activities

• PC: NSDI'19, SecDev'18.
• ERC: PLDI'18.
• Reviewer: Transactions on Computers, IET Software, Science China Information Sciences.

Selected Talks

Introduction to CertiKOS.

• Oct. 2017, New England Systems Verification Day, MA.

Building Fully Trustworthy OS Kernels through Formal Verification.

• Aug. 2017, University of Washinton, WA.
• Apr. 2017, Chicago University, 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.

• Nov. 2015, Yale Programming Languages Day, CT.
• June 2015, New England Programming Languages and Systems Symposium, CT.
• May 2015, High Confidence Software and Systems Conference, MD.
• Jan. 2015, POPL, Mumbai, India.

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

Teaching Experience

Asistant Professor at Columbia University.

• COMS E6998 Formal Verification of System Software (Fall 2018).
• COMS W3101 Programming Languages (Python) (Spring 2018).

Teaching Asistant at Yale University.

• 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).