Faculty Candidate Seminar

Formal Verification of a Concurrent File System

Tej ChajedPh.D. CandidateMIT
3725 Beyster BuildingMap

Zoom link for remote participants, passcode:  582688


Bugs in systems software like file systems, databases, and operating systems can have serious consequences, ranging from security vulnerabilities to data loss, and these bugs affect all the applications built on top. Systems verification is a promising approach to improve the reliability of our computing infrastructure, since it can eliminate whole classes of bugs through machine-checked proofs that show a system always meets its specification.

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 correctly follow the NFS protocol, 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.



Cindy Estell

Student Host

Eli Goldweber

Faculty Host

Manos Kapritsos