Verifying concurrent, crash-safe systems with Perennial

by Chajed, Tej, Tassarotti, Joseph, Kaashoek, M. Frans, Zeldovich, Nickolai
Published 2021

Argosy: verifying layered storage systems with recovery refinement

by Chajed, Tej, Tassarotti, Joseph, Kaashoek, M. Frans, Zeldovich, Nickolai
Published 2021

Using Crash Hoare logic for certifying the FSCQ file system

by Chen, Haogang, Ziegler, Daniel, Chajed, Tej, Chlipala, Adam, Kaashoek, M. Frans, Zeldovich, Nickolai
Published 2021

Certifying a file system using crash hoare logic

by Chajed, Tej, Chen, Haogang, Chlipala, Adam, Kaashoek, M. Frans, Zeldovich, Nickolai, Ziegler, Daniel Todd
Published 2019

Verifying a high-performance crash-safe file system using a tree specification

by Chen, Haogang, Chajed, Tej, Konradi, Alex, Wang, Stephanie, İleri, Atalay, Chlipala, Adam, Kaashoek, M. Frans, Zeldovich, Nickolai
Published 2021