In February 2021, the paper titled “CSim2: Compositional Top-down Verification of Concurrent Systems using Rely-Guarantee” from the School of Cyberspace Security of Zhejiang University was published in the journal “ACM Transactions on Programming Languages and Systems” (TOPLAS), and Zhejiang University is the affiliation of the corresponding author.
TOPLAS is a top international journal in the field of computer programming languages. It only accepts achievements that have made outstanding contributions to this field. TOPLAS is also listed as tier-A journal recommended by the China Computer Federation (CCF) in the field of software engineering/system software/programming language. TOPLAS only publishes about 20 papers every year. Up to now, there are only 5 papers from the Chinese Mainland in the TOPLAS journal as the first (corresponding) authors. This paper is the first paper from Zhejiang University published in the TOPLAS journal since its first publication in 1979.
Formal verification of security and functional correctness for multi-core and concurrent system software faces significant technical challenges. This paper applies mathematical logics and proposes a formal programming language as well as novel verification methods for the concurrent system, to solve the theoretical challenges for concurrency verification and the top-down development of concurrent systems. We have developed prototype tools that can be applied to fundamental software and systems, such as operating systems, blockchains, unmanned vehicles, avionics, aerospace.
ICSR of Zhejiang University has made many significant contributions in the fields of Internet of Things security, system security, data security, blockchain security, artificial intelligence security, and network security. ICSR published more than 100 papers in top international journals (e.g. IEEE/ACM Transactions TDSC, TIFS, ToN, TISSEC) and top international conferences (e.g. IEEE S&P, ACM CCS, USENIX Security, SIGCOMM, NDSS, IEEE INFOCOM), and won 11 outstanding paper awards. This paper is the result of collaborations between ICSR and the Cyberspace Security Laboratory of Nanyang Technological University (NTU) in Singapore. It is a new breakthrough made by ICSR of Zhejiang University in the direction of programming language security. ZJU and NTU have carried out deep collaboration in formal methods and operating system security for many years, and jointly published a number of influential academic papers in top international conferences on formal verification and top international journals on cybersecurity.