Binary-Compatible Verification of Filesystems with ACL2

Mihir Parang Mehta & William R. Cook
Filesystems are an essential component of most computer systems. Work on the verification of filesystem functionality has been focused on constructing new filesystems in a manner which simplifies the process of verifying them against specifications. This leaves open the question of whether filesystems already in use are correct at the binary level. This paper introduces LoFAT, a model of the FAT32 filesystem which efficiently implements a subset of the POSIX filesystem operations, and HiFAT, a...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.