Using Crash Hoare Logic for Certifying the FSCQ File System

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich. Using Crash Hoare Logic for Certifying the FSCQ File System. In Ajay Gulati, Hakim Weatherspoon, editors, 2016 USENIX Annual Technical Conference, USENIX ATC 2016, Denver, CO, USA, June 22-24, 2016. USENIX Association, 2016. [doi]

@inproceedings{ChenZCCKZ16,
  title = {Using Crash Hoare Logic for Certifying the FSCQ File System},
  author = {Haogang Chen and Daniel Ziegler and Tej Chajed and Adam Chlipala and M. Frans Kaashoek and Nickolai Zeldovich},
  year = {2016},
  url = {https://www.usenix.org/conference/atc16/technical-sessions/presentation/chen_haogang},
  researchr = {https://researchr.org/publication/ChenZCCKZ16},
  cites = {0},
  citedby = {0},
  booktitle = {2016 USENIX Annual Technical Conference, USENIX ATC 2016, Denver, CO, USA, June 22-24, 2016},
  editor = {Ajay Gulati and Hakim Weatherspoon},
  publisher = {USENIX Association},
}