Date & Time:
December 6, 2018 4:00 pm – 5:30 pm
Crerar 298, 5730 S. Ellis Ave., Chicago, IL,
12/06/2018 04:00 PM 12/06/2018 05:30 PM America/Chicago Frans Kaashoek (MIT) – Verifying a File System: Correctness in Presence of Crashes CERES Unstoppable Speaker Series Crerar 298, 5730 S. Ellis Ave., Chicago, IL,

Verifying a file system: correctness in
presence of crashes

As a case study of system software verification, this talk will describe FSCQ, the first file system with a machine-checkable proof (using the Coq proof assistant) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data. This talks describes how we wrote FSCQ's specification and how we proved that FSCQ's implementation meets its specification. Although FSCQ is a simple file system, our experience with FSCQ suggests that formal verification is ready for certifying system software, opening up many interesting and challenging research problems. Joint work with: Tej Chajed, Haogang Chen, Atalay İleri, Adam Chlipala, Nickolai Zeldovich.

Host: Haryadi Gunawi

Frans Kaashoek

Professor, Massachusetts Institute of Technology

Frans Kaashoek is the Charles Piper Professor in MIT's EECS department and a member of CSAIL, where he coleads the parallel and distributed operating systems (PDOS) group. He received his PhD from the Vrije Universiteit (Amsterdam, The Netherlands) for his work on group communication in the Amoeba distributed operating system. Frans is a member of the National Academy of Engineering and the American Academy of Arts and Sciences, the recipient of the ACM SIGOPS Mark Weiser award and the 2010 ACM Prize in Computing. He was a cofounder of Sightpath, Inc. and Mazu Networks, Inc.

Related News & Events

UChicago CS News

UChicago Computer Scientists Bring in Generative Neural Networks to Stop Real-Time Video From Lagging

Jun 29, 2023
UChicago CS News

UChicago Team Wins The NIH Long COVID Computational Challenge

Jun 28, 2023
UChicago CS News

UChicago Assistant Professor Raul Castro Fernandez Receives 2023 ACM SIGMOD Test-of-Time Award

Jun 27, 2023
UChicago CS News

Computer Science Displays Catch Attention at MSI’s Annual Robot Block Party

Apr 07, 2023
UChicago CS News

Professor Heather Zheng Named ACM Fellow

Jan 18, 2023
UChicago CS News

Q&A: Ian Foster on Receiving the 2023 IEEE Internet Award

Jan 06, 2023

Ian Foster – Better Information Faster: Programming the Continuum

Jan 06, 2023
UChicago CS News

Professor Fred Chong Named IEEE Fellow

Dec 09, 2022
UChicago CS News

Associate Professor Diana Franklin Named ACM Distinguished Member

Dec 07, 2022
UChicago CS News

UChicago’s Parsl Project Pivots to Sustainability and Community with New Grants

Nov 17, 2022
man browsing Netflix
UChicago CS News

Trending Now: How Netflix Chills Our Free Will

Nov 14, 2022
In the News

Alumnus Pranav Gokhale Named to Crain’s 40 Under 40

Nov 07, 2022
arrow-down-largearrow-left-largearrow-right-large-greyarrow-right-large-yellowarrow-right-largearrow-right-smallbutton-arrowclosedocumentfacebookfacet-arrow-down-whitefacet-arrow-downPage 1CheckedCheckedicon-apple-t5backgroundLayer 1icon-google-t5icon-office365-t5icon-outlook-t5backgroundLayer 1icon-outlookcom-t5backgroundLayer 1icon-yahoo-t5backgroundLayer 1internal-yellowinternalintranetlinkedinlinkoutpauseplaypresentationsearch-bluesearchshareslider-arrow-nextslider-arrow-prevtwittervideoyoutube