ACL2 Seminar, April 6, 2018

Speaker: Mihir Mehta

Title: Verifying the FAT32 filesystem with ACL2

Abstract: In this talk, we discuss an effort to verify filesystems with
ACL2, based on executable specifications available in kernel source code
and userland filesystem utilities. We detail one application of this
approach to the FAT32 filesystem through the construction of an
increasingly complex series of formally verified models. We explain the
degree to which these models are binary compatible with these executable
specifications and outline future work towards the goal of full binary
compatibility.