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

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