Campus Event Calendar

Event Entry

What and Who

Formal Methods for Systems Software: The Good, The Bad, The Ugly

Haibo Chen
Shanghai Jiao Tong University

Haibo Chen is a Distinguished Professor of Shanghai Jiao Tong University, where he founds and directs the Institute for Parallel and Distributed Systems (IPADS). His main research areas are operating systems, distributed systems and the application of formal methods. He received Best Paper Awards from SOSP, ASPLOS, EuroSys and VEE, Test of Time Award from DSN, Best Paper Honorable Mention and Research Highlight Award from SIGMOD, Honorable Mention of The Dennis M. Ritchie Thesis Award (Advisor) from SIGOPS. He currently chairs ACM SIGOPS, serves on the editorial board member of contributed articles and co-chairs  the Regional Special Sections of Communications of the ACM, co-chairs the program committee of EuroSys 2025, and chairs the inaugural technical steering committee of OpenHarmony, an open-source operating system deployed on hundreds of millions of devices. He is an ACM Fellow and IEEE Fellow.
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI  
AG Audience

Date, Time and Location

Friday, 19 April 2024
60 Minutes
E1 5


Formal methods have recently gained a resurgent interest in academia and industry due to the the increasing demand of high-assurance systems software. This can be evidenced by the increasing investment on formal methods in industry like Microsoft, Amazon and Huawei. In this talk, I will share our experiences in applying formal methods in verifying systems software. Specifically, I will describe the efforts in applying formal methods in the design and implementation synchronization primitives, file systems and distributed system protocols. Based on these, I will further describe the experiences and lessons learned in applying formal methods at a large-scale setting, and discuss possible challenges and opportunities in fostering better synergy between academia and industry.


Lena Schneider
+49 681 9303 9107
--email hidden

Virtual Meeting Details

966 8141 4048
passcode not visible
logged in users only

Lena Schneider, 04/10/2024 16:02 -- Created document.