April 2, 2007
InterSchool Lab, 7th floor CEPSR
Hosted by: CS Department
Speaker: Junfeng Yang, Stanford University
Storage systems such as file systems, databases, and RAID systems have a simple, basic contract: you give them data, they do not lose or corrupt it. Unfortunately, their code is exceptionally hard to get right: it must anticipate all failures and crashes, and always correctly recover from them, regardless of the current system state. In this talk, I will describe an approach we invented that makes it easy to systematically check real storage systems for errors. We used a novel adaption from model checking, a comprehensive, heavyweight formal verification technique, that makes our approach systematic while being lightweight. We applied this approach to a broad range of real storage systems, and found serious data-loss bugs in every system checked, typically with little effort.
Junfeng Yang is a Ph.D. candidate in the Computer Science Department at Stanford. His research interests span the areas of systems, security, software engineering and programming languages, focusing on practically checking large, real-world software systems. Junfeng Yang received his MS in Computer Science from Stanford in 2002, and his BS in Computer Science from Tsinghua University, Beijing, China in 2000. He is a receipt of the Siebel Scholarship, the Stanford School of Engineering fellowship. He received the Best Paper Award of OSDI 2004.