Wed 28 Oct 2015 14:37 - 15:00 at Grand Station 1 - 3. Verification Chair(s): Guangtai Liang

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.

Wed 28 Oct

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 15:00
3. VerificationOOPSLA at Grand Station 1
Chair(s): Guangtai Liang IBM Research - China
13:30
22m
Talk
Conditionally Correct Superoptimization
OOPSLA
Rahul Sharma Stanford University, Eric Schkufza Stanford University, Berkeley Churchill Stanford University, Alex Aiken Stanford University
DOI
13:52
22m
Talk
Selective Control-Flow Abstraction via JumpingOOPSLA Artifact
OOPSLA
Sam Blackshear University of Colorado at Boulder, USA, Bor-Yuh Evan Chang University of Colorado at Boulder, USA, Manu Sridharan Samsung Research America
Link to publication
14:15
22m
Talk
Automating Grammar ComparisonOOPSLA Artifact
OOPSLA
Ravichandhran Madhavan EPFL, Switzerland, Mikaël Mayer EPFL, Switzerland, Sumit Gulwani Microsoft Research, USA, Viktor Kunčak EPFL, Switzerland
Link to publication
14:37
22m
Talk
Reasoning about the POSIX File System: Local Update and Global Pathnames
OOPSLA
Gian Ntzik Imperial College London, UK, Philippa Gardner Imperial College London, UK
DOI