一句话：在 Coq 中建立自稳定算法的通用认证框架，并验证 k-聚类算法的部分正确性与簇头数量上界。
本文针对分布式自稳定算法正确性证明复杂、难以机器验证的问题，提出在 Coq 证明助手中构建经验证证明的通用框架。作者首先形式化了自稳定领域常用的复合原子性局部共享内存模型，并开发了包含势函数、集合基数等通用工具的库。为验证框架，他们对一个已有的静默自稳定 k-聚类算法进行了认证，证明其非平凡部分正确，并给出输出聚类簇头数量的定量界：当网络有 n 个节点时，簇头数至多 floor((n-1)/(k+1))+1。该工作为自稳定算法的机器化验证提供了可复用基础。
We propose a general framework to build certified proofs of distributed self-stabilizing algorithms with the proof assistant Coq. We first define in Coq the locally shared memory model with composite atomicity, the most commonly used model in the self-stabilizing area. We then validate our framework by certifying a non trivial part of an existing silent self-stabilizing algorithm which builds a $k$-clustering of the network. We also certify a quantitative property related to the output of this algorithm. Precisely, we show that the computed $k$-clustering contains at most $\lfloor \frac{n-1}{k+1} \rfloor + 1$ clusterheads, where $n$ is the number of nodes in the network. To obtain these results, we also developed a library which contains general tools related to potential functions and cardinality of sets.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AltisenCD17,
title = {A Framework for Certified Self-Stabilization},
author = {Karine Altisen and Pierre Corbineau and Stephane Devismes},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:14)2017}
}