Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Overview
  • Workshop Organizers
  • Workshop Program
  • Sponsorship
  • Instructions for Participants
  • Call for Papers
  • Past Workshops

sponsors

Bronze Sponsor
Bronze Sponsor
Bronze Sponsor

connect with us


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Specifying Crash Safety for Storage Systems
Tweet

connect with us

Specifying Crash Safety for Storage Systems

Tuesday, May 19, 2015 - 3:00pm-3:30pm
Authors: 

Haogang Chen, Daniel Ziegler, Adam Chlipala, and M. Frans Kaashoek, MIT CSAIL; Eddie Kohler, Harvard University; Nickolai Zeldovich, MIT CSAIL

Abstract: 

Software that is provably correct has been a long-time goal of computer science. Until recently this goal was realized for only small programs, but over the last decade several large systems have been built that have provable correctness properties. Examples include CompCert, seL4, IronClad, CertiKOS, Bedrock, Termite, Click’s dataplane, and Jitk. One aspect not covered by these systems is reasoning about failures—power failures, hardware faults, or software bugs—which is well-known to be tricky in systems code.

Haogang Chen, MIT CSAIL

Daniel Ziegler, MIT CSAIL

Adam Chlipala, MIT CSAIL

M. Frans Kaashoek, MIT CSAIL

Eddie Kohler, Harvard University

Nickolai Zeldovich, MIT CSAIL

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {189922,
author = {Haogang Chen and Daniel Ziegler and Adam Chlipala and M. Frans Kaashoek and Eddie Kohler and Nickolai Zeldovich},
title = {Specifying Crash Safety for Storage Systems},
booktitle = {15th Workshop on Hot Topics in Operating Systems (HotOS XV)},
year = {2015},
address = {Kartause Ittingen, Switzerland},
url = {https://www.usenix.org/conference/hotos15/workshop-program/presentation/chen_haogang},
publisher = {USENIX Association},
month = may,
}
Download
Chen Haogang PDF
  • Log in or    Register to post comments

Bronze Sponsors

© USENIX

  • Privacy Policy
  • Contact Us