USTC-Yale Joint Research Center for High-Confidence Software has made great progress in its research. The Center was founded in October 2008. It is based on the original Software Security Lab in School of Computer Science and Technology, with supports and collaborations from Professor Zhong Shao's Flint Group at Yale University. The goal is to build a world-wide top research center in the area of high-confidence software. Now the Center has partly achieved the goal after several years of efforts. The current research group of the Center is led by USTC's Professor Xinyu Feng, who got his PhD from Yale University. Till now researchers in the Center have published several papers in top-level international conferences in Computer Science. Also the collaborations between USTC and Yale have expanded to other related research areas, including computer network and operating systems.
In mid-June this year, the PhD student Hongjin Liang and her advisor Professor Xinyu Feng published the paper titled "Modular Verification of Linearizability with Non-Fixed Linearization Points" in the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13). PLDI is one of the top conferences in Computer Science. The first PLDI was held in 1979. Now it is a forum where researchers, developers, educators, and practitioners exchange information on the latest practical and experimental work in the design and implementation of programming languages. It emphasizes innovative and creative approaches to compile-time and runtime technology; novel language designs and features; and results from implementations. It accepts about 30 - 40 papers each year, and before this year, there are no more than five accepted papers from Chinese mainland.
In their paper, Hongjin Liang and Xinyu Feng proposed a program logic to verify linearizability of concurrent algorithms. Their approach is very practical. It can be applied to algorithms with non-fixed linearization points, which are very difficult to verify in the literature. The reviewers highly recognized the contributions of their work and said, "the proof system itself is a significant contribution ... It is good to hear that all these algorithms can be verified by this work", "The paper also has one new contribution, the try-commit commands for specifying future dependent linearization points, which (despite its apparent simplicity) is rather nice and worthy of publication", etc. The experts who attended the conference also highly regarded this work.
Actually in January 2012, Hongjin Liang and Xinyu Feng (with Ming Fu, a PostDoc of the Center) have published a paper in the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12). This is the first paper accepted by the top conference POPL whose first affiliation is from Chinese mainland. Moreover, Hongjin Liang and Xinyu Feng also have a paper published on the 24th International Conference on Concurrency Theory (CONCUR'13), which is joint work with Jan Hoffmann and Professor Zhong Shao from Yale University. CONCUR is also a respected conference in this area.
There is other collaborative work of the Center published on top conferences. For instance, the paper titled "Maple: Simplifying SDN Programming Using Algorithmic Policies" has published in SIGCOMM'13. The PhD student Junchang Wang from USTC and the Center (whose advisor is Professor Bei Hua) is the second author of this paper. This is joint work with Andreas Voellmy, Y. Richard Yang, Bryan Ford and Paul Hudak from Yale University.
Their work is about Software-Defined Networking (SDN), which is a breakthrough notion in computer networking. It allows a network to customize its behaviors through centralized policies at a conceptually centralized network controller. Their work Maple gives a powerful, programmer-friendly SDN programming model. It enables a programmer to use standard algorithmic programming to design arbitrary algorithms for SDN control, without thinking about lower level issues. The reviewers highly recognized this work and said, "too good to know that it can be true". The paper was nominated as the best paper.
In addition to fundamental research, the Center is also planning to collaborate with industry, under the supports from USTC and our School of Computer Science and Technology. The Center encourages its members with strong research background to develop certified software and operating systems and related verification tools.
