Imperial College London
Alternate

ProfessorPhilippaGardner

Faculty of Engineering, Department of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Ntzik:2015:10.1145/2814270.2814306,
author = {Ntzik, G and Gardner, P},
doi = {10.1145/2814270.2814306},
pages = {201--220},
publisher = {ACM},
title = {Reasoning about the POSIX file system: Local update and global pathnames},
url = {http://dx.doi.org/10.1145/2814270.2814306},
year = {2015}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including '..' and symbolic links) which may overlap the directories being updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no '..' or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.
AU  - Ntzik,G
AU  - Gardner,P
DO  - 10.1145/2814270.2814306
EP  - 220
PB  - ACM
PY  - 2015///
SP  - 201
TI  - Reasoning about the POSIX file system: Local update and global pathnames
UR  - http://dx.doi.org/10.1145/2814270.2814306
UR  - http://hdl.handle.net/10044/1/25827
ER  -
Download