Verified Systems Software
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
Bellevue, WA, US
Zürich, ZH, Switzerland
2022 Interns
2020 Interns
External Researchers
- Andrea Lattuada*
- Bryan Parno
- Chris Hawblitzel
Related Publications
- Linear Types for Large-Scale Systems Verification April, 2022
- Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion 2022
- Induction Duality: Primal-Dual Search for Invariants January, 2022
Category
- Active Research Projects