The First Paper from Chinese Mainland Accepted by POPL

Recently, LIANG Hongjin, FENG Xinyu and FU Ming from USTC-Yale Joint Research Center for High-Confidence Software had a paper "A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations" accepted by the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). This is the first paper accepted by POPL whose first affiliation is from Chinese mainland, and University of Science and Technology of China (USTC) becomes the first institution receiving the honor.

POPL is one of the top international conferences on programming languages and systems. It is an annual forum for the discussion of programming language design and implementation, compilers, program analysis and verification, etc.

The first author LIANG Hongjin is currently a PhD student from School of Computer Science and Technology in USTC, advised by Prof. FENG Xinyu. Their paper presents a general method for verifying concurrent program transformations. Inspired by the rely-guarantee verification method for concurrent programs, they parameterize the traditional simulations with rely-guarantee conditions, successfully support compositional verification of concurrent program transformations and finally apply their method to verify compiler optimization, implementation of concurrent data structures and concurrent garbage collection algorithms. The reviewers highly recognized the contributions of their work and said, "I found this to be a compelling paper. Combining simulation techniques with rely-guarantee reasoning seems like a good idea, and I haven' t seen this elsewhere … This work would provide a nice unifying theory for concurrent program transformations", "I like this paper … Refinement in a concurrent setting is very challenging and this paper makes a good step into that field", "A logic that can support both the runtime system verification and the compiler verification simultaneously would be very useful. This paper presents such a logic, and it looks like a very general and natural approach", etc.

Established in 2008, USTC-Yale Joint Research Center for High-Confidence Software combines the expertise of faculty members from USTC and Yale University with the facilities and human resources of USTC. Leading by Prof. FENG Xinyu, the Center would become one of the top research institutions in the areas of high-confidence software.