معرفی
Zhong Shao is the Thomas L. Kempner Professor of Computer Science at Yale University. He leads the FLINT research group and is a prominent researcher in programming languages, formal methods, operating systems, and computer security. His work focuses on building certified system software through mechanized proofs to create dependable software systems that can manage increasing complexity in modern computing.
Professor Shao's research spans multiple domains including programming language design, OS kernel development, formal semantics, compiler construction, and proof engineering. His work addresses challenging problems in concurrency and distributed computing, with a particular emphasis on creating hacker-resistant systems. He has collaborated with researchers at Princeton, University of Pennsylvania, and MIT on the NSF Expedition project 'The Science of Deep Specification.'
Shao's recent publications demonstrate a strong focus on compositional verification techniques for distributed systems and certified compilation. His work on DeepSEA language, CertiKOS operating system, and various verification frameworks shows a consistent trajectory toward building fully verified system software from the ground up. Key themes include linearizability, Byzantine fault tolerance, compositional reasoning, and refinement-based verification approaches across concurrent and distributed systems.
As an educator, Professor Shao teaches courses including CS430 Formal Semantics (Spring 2025), CS421 Compilers and Interpreters, CS422 Operating Systems, and CS428 Language-Based Security. He participates in systems seminars on APLAR and SPAM, contributing to the academic community through both research and teaching.
Professor Shao leads the FLINT research group at Yale, which focuses on building novel certified system software. The group's work has resulted in breakthroughs such as the CertiKOS operating system, which represents a significant advancement in hacker-resistant concurrent operating systems. The group collaborates with the DeepSpec project, an NSF Expedition focused on deep specifications for trustworthy systems, and has developed frameworks like LiDO, Adore, and AdoB for verifying distributed systems with strong guarantees.
