ACL2 Seminar, 10/27/2017

Speaker: Mihir Mehta

Title: Verifying filesystems in ACL2

Abstract: In this talk, we discuss an ongoing effort to model real-world
filesystems in ACL2 with a goal of binary compatibility at the disk
image level, proving the correctness of these models along the way. We
discuss the challenges encountered so far in modelling a simple
filesystem with an external disk, immediate future plans to verify the
checking of permissions for each access, and future plans to use such a
verified model as a basis for analysing the correctness (or lack
thereof) of tools such as fsck.