Loading Events

« All Events

  • This event has passed.

CIS Seminar: “Formal verification of a concurrent file system”

March 24 at 3:30 PM - 4:30 PM

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.

Tej Chajed

CSAIL, MIT

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.

Details

Date:
March 24
Time:
3:30 PM - 4:30 PM
Event Tags:
Website:
https://www.cis.upenn.edu/events/

Organizer

Computer and Information Science
Phone:
215-898-8560
Email:
cis-info@cis.upenn.edu
View Organizer Website

Venue

Wu and Chen Auditorium (Room 101), Levine Hall
3330 Walnut Street
Philadelphia, PA 19104 United States
+ Google Map
View Venue Website