paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Compiling Distributed System Models with PGo

用 PGo 编译分布式系统模型
ASPLOS Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22023匹配度 2/10 · 论文聚焦分布式系统形式模型到可执行实现的编译与代码生成，属于形式方法与编程语言交叉，但未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析，也不以机器学习/Agentic 程序为对象；仅与“形式化+工程实现”的偏好有弱关联。引用 11 inbox
Finn Hackett, Shayan Hosseini, Renato Costa, Matthew Do, Ivan Beschastnikh
领域特定语言与建模编译与代码生成分布式与容错
crossref: 2026-09-12

AI 速览

一句话：提出 PGo，将分布式系统模型编译为可执行实现，以减少形式设计与实现之间的人工桥接。

分布式系统的设计与实现难以保证正确性，形式化方法正被用于该领域，但其核心挑战在于形式设计与实现之间缺少直接联系，目前多依赖手工桥接。本文围绕 PGo 展开，题目表明其将分布式系统模型编译为可执行代码，从而减少人工迁移，使实现更贴近形式模型。给出的摘要未展开具体编译机制、支持的语言或模型，也未给出实验评估；因此方法和结果细节需参阅论文正文。

问题
分布式系统正确实现困难，形式化设计与实现之间缺少自动连接，当前主要依靠手工桥接。
方法
提出/研究 PGo 这一编译方案，将分布式系统模型编译为可执行代码，以在形式模型与实现之间建立编译路径；具体机制未在摘要中说明。
评估
给出的摘要未描述评估方式；无法从现有材料得知实验、案例研究或基准测试等细节。
原文摘要（Abstract）

Distributed systems are difficult to design and implement correctly. In response, both research and industry are exploring applications of formal methods to distributed systems. A key challenge in this domain is the missing link between the formal design of a system and its implementation. Today, practitioners bridge this link through manual effort.

链接与引用

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

BibTeX 
@inproceedings{paperbot9993,
  title = {Compiling Distributed System Models with PGo},
  author = {Finn Hackett and Shayan Hosseini and Renato Costa and Matthew Do and Ivan Beschastnikh},
  booktitle = {ASPLOS},
  year = {2023},
  doi = {10.1145/3575693.3575695}
}