paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Black Ninjas in the Dark

黑暗中的黑忍者
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 3/10 · 论文涉及程序验证，与用户对形式化验证的兴趣有弱关联；但研究对象是分布式计算中的种群协议，不属于静态分析、Agentic/LLM 程序分析、浮点程序分析或贝叶斯程序分析等核心方向。引用 5 inbox
Michael Blondin, Javier Esparza, Stefan Jaax, Antonín Kučera
分布式与容错程序验证
crossref: 2026-09-12

AI 速览

一句话：以交互式论文形式介绍种群协议这一分布式计算基础模型，并综述作者近期关于其自动验证的工作。

本文是一篇交互式论文，建议联网阅读。它面向读者介绍种群协议（population protocols）——分布式计算的一个基础模型，并介绍作者及其同事近期关于种群协议自动验证的工作。论文本身不提出新的算法或定理，而是以交互形式组织已有研究，帮助读者理解该模型及其验证问题。由于摘要未给出具体技术细节与实验结果，本文的核心贡献在于教学性、综述性与可交互的呈现方式，而非实证评估。

问题
向读者介绍种群协议这一分布式计算基础模型，并呈现作者及其同事在种群协议自动验证方面的近期工作。
方法
采用交互式论文形式，建议联网阅读，以综述和教学方式组织种群协议及自动验证研究。
评估
摘要未给出实验或基准评估；本文以交互式阅读和综述呈现为主，未涉及实证评估。
原文摘要（Abstract）

In this interactive paper, which you should preferably read connected to the Internet, the Black Ninjas introduce you to population protocols, a fundamental model of distributed computation, and to recent work by the authors and their colleagues on their automatic verification.

链接与引用

DOI 原文 ·

BibTeX 
@inproceedings{paperbot4345,
  title = {Black Ninjas in the Dark},
  author = {Michael Blondin and Javier Esparza and Stefan Jaax and Antonín Kučera},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209110}
}