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/.