ACL2 Seminar, 4/28/2017

Speaker: Mihir Mehta

Title: Verifying filesystems in ACL2

Abstract: Modern filesystems are growing more reliable against data
loss, data corruption and data races in multiprogramming environments;
however, this comes at the cost of increased complexity of
implementation and a higher vulnerability to bugs. In this talk, we
describe a work in progress to incrementally build a verified model of a
filesystem that is binary compatible with the CP/M filesystem, and our
future plans to model more complex filesystems including FAT32.