Introduction

Develop fast systems software with zero bugs

Summary

We want to make verification (statically-checked functional correctness) a practical development methodology.

We're building a verified version of the high-performance BetrFS file system. We want users to trust their data to BetrFS, a fast new file system, because it's proven to have no data loss or corruption bugs. We're using our experience to improve verification tools to make verified development a viable alternative to test-driven development. The approach is especially valuable for software where latent bugs are very painful, like data loss bugs in a file system.

Details

Our OSDI 2020 publication describes our initial effort building the key-value store that underlies BetrFS. We are actively working on:
  • optimizing performance
  • adding support for multi-core concurrency
  • improving the linear type system that eases reasoning about alias-freedom
  • building filesystem semantics and coupling to the Linux kernel

Researchers

2020 Interns

External Researchers

  • Bryan Parno
  • Chris Hawblitzel

Related Publications

Category

  • Active VMW Software Systems Projects

Research Areas

  • filesystems
  • storage
  • verification