paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Challenges and Opportunities in Model Checking Large-scale Distributed Systems

大规模分布式系统模型检测的挑战与机遇
ICSE Proceedings of the IEEE/ACM 46th International Conference on Software Engineering2024匹配度 4/10 · 论文关注工业级分布式系统的模型检查与形式化验证，符合用户对形式化验证和工业落地的兴趣，但不涉及 LLM/Agent 与静态分析/形式化验证的交叉，也非浮点程序分析或贝叶斯程序分析，因此与核心研究方向匹配有限。引用 0 inbox
Rupak Majumdar
程序验证分布式与容错
crossref: 2026-09-12

AI 速览

一句话：概述 Must 项目为工业级分布式系统提供设计验证支持的目标、技术特征与学术转工业经验。

本文介绍 Must 项目，其目标是为工业规模的分布式系统提供设计与验证支持。论文概述了项目的设计目标、技术特性，以及研究团队在将学术研究成果转化为工业工具过程中所获得的经验教训。摘要未报告具体算法细节或量化基准，而是从项目层面讨论模型检测在大型分布式系统场景下面临的挑战与机遇，并总结学术研究落地为工业工具时需要考虑的工程与实践问题。

问题
如何为工业规模的分布式系统提供有效的设计与验证支持，并解决将学术模型检测研究转化为工业工具时遇到的挑战。
方法
以 Must 项目为对象，概述其设计目标与技术特征，并总结从学术研究到工业工具转移过程中的经验教训。
评估
基于项目实践进行经验性总结与反思，而非报告具体的量化实验或基准评测结果。
原文摘要（Abstract）

The goal of the Must project is to provide design and verification support for industrial-scale distributed systems. We provide an overview of the project: its design goals, its technical features, as well as some lessons we learnt in the process of transferring academic research to an industrial tool.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot11300,
  title = {Challenges and Opportunities in Model Checking Large-scale Distributed Systems},
  author = {Rupak Majumdar},
  booktitle = {ICSE},
  year = {2024},
  doi = {10.1145/3597503.3649398}
}