报告题目：用霍尔逻辑证明文件系统在宕机下的正确性

报告人：陈昊罡博士

报告时间：2020年01月17日10:00

报告地点：数计学院2号楼309报告厅

陈昊罡博士，于美国麻省理工学院获得计算机科学博士学位，于北京大学获得计算机科学硕士和学士学位。主要研究方向为操作系统、分布式系统、系统安全和可靠性。曾在计算机系统领域著名会议SOSP和OSDI发表过多篇学术论文，现就职于美国旧金山的大数据公司Databricks，带领技术团队为企业用户提供基于公有云和Spark的大数据分析解决方案。

  FSCQ是第一个提供了机器可检验的、经过形式化证明的文件系统。FSCQ用形式化证明的方法避免了困扰现有文件系统的错误，例如在没有同步的情况下执行磁盘写操作或忘记将目录块清零。FSCQ的定理证明，在发生任何崩溃然后重新启动的情况下，FSCQ都能正确恢复文件系统的状态且不会丢失数据。