Local Reasoning for the POSIX File System
Authors
- Philippa Gardner
- Gian Ntzik
- Adam Wright
Abstract
We provide a program logic for specifying a core subset of the sequential POSIX file system, and for reasoning abstractly about client programs working with the file system.