使用 TLA+ 三件套进行规约与验证：TLC、Apalache 与 TLAPS
计算机科学中的逻辑
2022-11-15 v1
摘要
以 Safra 提出的分布式终止检测算法为贯穿示例，我们介绍了用于验证 TLA+ 所写规约的主要工具。通过考察它们互补的优势与弱点，我们提出了一种支持不同类型分析并可适应所需置信度的工作流。
引用
@article{arxiv.2211.07216,
title = {Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS},
author = {Igor Konnov and Markus Kuppe and Stephan Merz},
journal= {arXiv preprint arXiv:2211.07216},
year = {2022}
}