Formal verification of a concurrent file system
In this talk, I’ll present a line of work culminating in a verified, concurrent file system called DaisyNFS. The file system comes with a proof that shows operations appear to execute correctly and atomically (that is, all-or-nothing), even if the computer crashes and when processing concurrent operations. I’ll describe how a combination of design and verification techniques make it possible to carry out the proof for an efficient implementation.
Bio: Tej Chajed is a final-year PhD student at MIT advised by Frans Kaashoek and Nickolai Zeldovich. His research is on systems verification, ranging from developing new foundations through designing and verifying high-performance systems. Before MIT, he completed his undergraduate degree in Electrical Engineering and Computer Science at UIUC. His work has been in part supported by an NSF graduate research fellowship.
This talk will be recorded and live-streamed at https://mediacentrallive.princeton.edu/.