- Philippa Gardner
- Gian Ntzik
- Adam Wright
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.
Proceedings of the 23rd European Symposium on Programming (ESOP’14), pp. 169–188