Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich. Using Crash Hoare logic for certifying the FSCQ file system. In Ethan L. Miller, Steven Hand, editors, Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015. pages 18-37, ACM, 2015. [doi]
Abstract is missing.