This page is part of an archival collection and is no longer actively maintained.

It may contain outdated information and may not meet current or future WCAG accessibility standards. We provide this content, its subpages, and associated links for historical reference only. If you need assistance, please contact support@cs.washington.edu

UNSAT: Yggdrasil

Yggdrasil

Yggdrasil is a toolkit for writing file systems with push-button verification. Yggdrasil asks programmers for three inputs: a specification of the expected behavior, an implementation, and consistency invariants indicating whether a file system image is in a consistent state. It then performs verification to check if the implementation meets the specification. If there is a bug, Yggdrasil produces a counterexample to help identify and fix the cause. If the verification passes, Yggdrasil produces an executable file system. Yggdrasil achieves this automation through a novel definition of file system correctness called crash refinement; it is amenable to SMT reasoning and enables developers to implement file systems in a modular way for verification.

Publications

  • Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button Verification of File Systems via Crash Refinement. In Proc. of the 12th OSDI, Nov 2016. [pdf] [slides] Best paper award

Software

The source code is hosted on GitHub at https://github.com/locore/yggdrasil/.