Recently, Hongjin Liang, Xingyu Feng, and Ming Fu from USTC-Yale Joint Research Center for High-Confidence Software had an important progress in refinement verification of concurrent program. Their paper titled “Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations” was published in ACM Transactions on Programming Languages and Systems (TOPLAS).
Program refinement establishes a relation between a concrete program and a more abstract one. It is a theoretical foundation for program verification. The refinement of concurrent program is one of the main challenges in this field. The refinement relation between individual sequential threads cannot be preserved in general with the presence of parallel compositions. On the other hand, the refinement relation defined based on fully abstract semantics of concurrent programs assumes arbitrary parallel environments, which is too strong and cannot be satisfied by many well-known transformations.
Liang et. al proposed the RGSim to verify concurrent program transformations. Their paper titled “Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations” was published in ACM Transactions on Programming Languages and Systems (TOPLAS). TOPLAS is the premier journal for reporting recent research advances in the areas of programming languages, and systems to assist the task of programming. Before Liang et. al, the only full paper from China mainland was published by Institute of Software CAS in 1993. Researchers of Peking University published a 3-page short paper in 1997.
In addition, Liang et. al published the first paper from China mainland in ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) in 2012. They also published a paper in ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) in 2013. These papers describe the theory and application of refinement verification of concurrent program.
Liang is currently a Ph.D. student of the School of Computer Science, advised by Professor Xingyu Feng.
(FU Hao, School of Computer Science and Technology)
