Zhong Shao

Professor Zhong Shao is working with the Computer Science Theory Group at Tsinghua University (led by Turing Award Laureate Professor Andrew Yao) to develop new formal methods and language-based technologies for building certified software. A certified software consists of the usual machine executable plus a rigorous machine-checkable proof (also represented inside the computer) that the software satisfies the desirable specification. Professor Shao's FLINT group hosted a visiting Ph.D. student from Tsinghua in the fall of 2005 and a visiting scholar in 2007; together they have worked out a new method for verifying arbitrary machine-level programs including operating system kernels.

Professor Zhong Shao collaborates with colleagues from the University of Science and Technology of China (USTC) to develop new technologies for building high-confidence software. He was recently appointed as an Honorary Guest Professor at USTC. Members of Professor Shao's FLINT group at Yale and Professor Yiyun Chen's group at USTC have been using the Coq proof assistant to develop a certified libraries for proof-carrying code. They recently developed a new framework for modular verification of assembly code with stack-based control abstractions. They have also worked out a new way of verifying garbage collectors and linking it with typed assembly languages.