UW CSE continued our winning ways this week with a Best Paper Award at the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’16). The winning paper, Push-Button Verification of File Systems via Crash Refinement, was co-authored by a team of researchers from UW CSE’s Computer Systems Lab and Programming Languages & Software Engineering (PLSE) group that includes Ph.D. students Helgi Sigurbjarnarson and James Bornholt, and professors Emina Torlak and Xi Wang.
The paper presents Yggdrasil, an efficient and practical new toolkit that will enable programmers to build reliable storage applications using push-button verification. The toolkit requires no manual annotations or proofs about the implementation code. To define file system correctness, Yggdrasil uses crash refinement, which is amenable to fully automated reasoning with satisfiability modulo theories (SMT) solvers. Yggdrasil offers several techniques to scale up automated verification, including a stack of abstractions and separation of data representations, so that developers can implement file systems in a modular way for verification. Yggdrasil also generates a concrete test case (a counterexample) in instances where it finds a bug in the file system implementation or its consistency invariants.
The team’s Best Paper Award is one of three given out at this year’s conference, which is taking place this week in Savannah, Georgia. It is not the only one with a UW CSE connection: former postdoc Simon Peter, now on the faculty of the University of Texas at Austin, co-authored one of the other winning papers, Ryoan: A Distributed Sandbox for Untrusted Computation on Secret Data.
With this latest win, UW CSE has completed the trifecta of top systems and networking conferences this year, having also earned Best Paper accolades at NSDI and SIGCOMM.
Go team!