回溯见证：单调状态的基础与应用
编程语言
2017-11-10 v3 密码学与安全
摘要
我们提供了一种方法，以简化状态单调演化的程序的验证。主要思想是，如果（1）状态按照给定的预序演化，且（2）性质被该预序保持，则在先前状态中被见证的性质可以在当前状态中可靠地回溯。在许多场景中，这种单调推理能产生简洁的模块化证明，省去了显式程序不变量的需要。我们将该方法提炼为单调状态幂，一个用于在依赖类型语言中进行 Hoare 风格单调状态推理的通用而紧凑的接口。我们证明了单调状态幂的可靠性，并将其作为在 F* 验证系统中推理单调状态的统一基础。基于此基础，我们构建了各种可变数据结构的库，如单调引用，并将这些库大规模应用于多个分布式应用的验证。
引用
@article{arxiv.1707.02466,
title = {Recalling a Witness: Foundations and Applications of Monotonic State},
author = {Danel Ahman and Cédric Fournet and Catalin Hritcu and Kenji Maillard and Aseem Rastogi and Nikhil Swamy},
journal= {arXiv preprint arXiv:1707.02466},
year = {2017}
}
备注
POPL'18 camera ready