这篇论文介绍了一个名为Serval的框架，用于通过符号执行来对系统代码进行可扩展的自动化验证。

Serval的核心思想是将开发人员使用Rosette编写指令集解释器并转化为自动化验证器，从而实现系统软件的验证。这一框架通过符号性能分析和优化来识别和修复验证性能瓶颈。作者通过将Serval应用于现有的系统和未经验证的系统中，展示了其在找到系统错误和提高验证效率方面的有效性。

本文提出了一个名为 SibylFS 的文件系统行为规范，可以以黑盒测试方式检查文件系统实现和规范之间的行为差异。

本文介绍了基于现代文件系统的应用层崩溃一致性协议的首个全面研究。研究发现，应用程序使用复杂的更新协议来持久化状态，而这些协议的正确性高度依赖于底层文件系统的微妙行为，我们称之为持久性属性。作者开发了一个名为BOB的工具来测试持久性属性，并使用它来证明这些属性在六种流行的Linux文件系统中存在广泛的差异。作者还构建了一个名为ALICE的框架，分析应用程序更新协议并发现崩溃漏洞，即需要特定持久性属性才能保证正确性的更新协议代码。使用ALICE，作者分析了11个广泛使用的系统，并发现了60个漏洞，其中许多会导致严重后果。作者还展示了ALICE可以用于评估新文件系统设计对应用程序级一致性的影响。

鉴于经常需要配置环境，在此记录一下 zsh & oh-my-zsh 的常用命令。

修改xv6的内核接口，构建状态机规范和声明式规范以支持SMT（Satisfiability Modulo Theories）求解器来进行验证。通过有限化内核接口，使用硬件虚拟化简化虚拟内存推理，并在LLVM IR级别工作，以避免对C语义进行建模，从而实现了"一键验证"。

主要思路是统计多个文件系统的实现，计算具体文件系统与多个文件系统总体之间的差异性（直方图/信息熵），从而窥探出其文件系统的具体实现在语义上的差异。