谷晓松博士生的论文获得第 41 届国际可靠分布式系统会议 SRDS'22 唯一最佳论文奖

国际可靠分布式系统会议 (International Symposium on Reliable Distributed Systems, SRDS) 公布大会奖项，南京大学计算机软件研究所团队的论文《Compositional Model Checking of Consensus Protocols Specified in TLA+ via Interaction-Preserving Abstraction》获得了该会议的唯一最佳论文奖 (Prof. C. V. Ramamoorthy Best Paper Award)。

论文针对模型检验中面临的状态爆炸问题，提出了一种分布式系统 TLA+ 规约的组合模型检验技术 IPA（Interaction-Preserving Abstraction）。IPA 技术针对分布式系统 TLA+ 规约的特点，提出通过模块划分、保交互抽象和模块组合完成组合模型检验的方法，证明组合模型检验的正确性，有效降低了模型检验的复杂度。团队将 IPA 技术应用到经典分布共识协议 Raft 和阿里巴巴云数据库 PolarDB 的分布共识协议 ParallelRaft 的正确性保障中，展示了 IPA 技术的可行性与有效性。该工作 Raft 部分的规约已公开，仓库地址：https://github.com/Disalg-ICS-NJU/IPA。

SRDS 是分布式系统可靠性领域历史悠久的重要国际会议，也是中国计算机学会推荐的 B 类学术会议，迄今已举办 41 届。通常，每年该会从所有录用论文中遴选出唯一最佳论文。此次获得最佳论文奖的工作由南大软件所团队与阿里巴巴 PolarDB 数据库团队合作完成，本文作者为南京大学的谷晓松博士生、黄宇教授、马晓星教授和阿里巴巴的曹伟、朱一聪、宋璇三位数据库技术专家。