Colloquium Details
Formal verification of a concurrent file system
Speaker: Tej Chajed, MIT
Location: 60 Fifth Avenue 150
Date: March 4, 2022, 11 a.m.
Host: Jinyang Li
Synopsis:
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 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.
Speaker 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.
Notes:
In-person attendance only available to those with active NYU ID cards.