Zhong Shao

Zhong Shao

Thomas L. Kempner Professor of Computer Science, Yale University

Welcome to my home page! I am interested in doing research on programming languages, formal methods, operating systems, and computer security. I am an advocate of certified software. I believe that certified programming with mechanized proofs is the most promising approach toward building truly dependable software and taking control of the rapidly growing complexity in future computer systems.

I lead the FLINT group at Yale. We are interested in building novel certified system software. Our work spans many fields, ranging from programming language design, realistic OS kernel hacking, formal semantics and logics, compiler development, and proof engineering, to solving difficult problems related to all aspects of concurrency and distributed computing.

I have also worked with researchers at Princeton, U. Penn, and MIT on the new NSF Expedition project: The Science of Deep Specification.

Check out our recent POPL'15 paper on Deep Specifications and Certified Abstraction Layers and PLDI'18 paper on Certified Concurrent Abstraction Layers for an overview of our new layered approach for building certified software. See our new CACM Research Highlight paper (and the original OSDI'16 paper and the official Yale press release) for an overview of our latest breakthrough on building certified hacker-resistant concurrent operating systems.

I am looking for new PostDocs and PhD students.   Feel free to contact me if you have interests in or around my research areas, are creative and highly motivated, and have strong technical skills.

I will be teaching CS430 Formal Semantics in Spring 2025. In the past I also taught CS112 Introduction to Programming, CS421 Compilers and Interpreters,CS422 Operating Systems, CS428/528 Language-Based Security, and CS210 A Second Course in Programming. I also attend the systems seminars on APLAR and SPAM.