在ACL2定理证明器中形式化文件系统：以FAT32为例的应用
计算机科学中的逻辑
2018-10-11 v1 操作系统
摘要
在这项工作中，我们提出了一种方法，用于在定理证明环境中构建现有文件系统的可执行规范并验证其功能属性。我们详述了该方法在FAT32文件系统上的应用。我们还详述了通过一系列逐步增加目标文件系统特性的模型来构建此类可执行规范的方法论。该方法论的好处在于，验证工作可从封装了许多文件系统共有特性、因而适合复用的简单模型开始。
引用
@article{arxiv.1810.04309,
title = {Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32},
author = {Mihir Parang Mehta},
journal= {arXiv preprint arXiv:1810.04309},
year = {2018}
}
备注
In Proceedings ACL2 2018, arXiv:1810.03762