Author of the publication

Certifying a file system using crash hoare logic: correctness in the presence of crashes.

, , , , , and . Commun. ACM, 60 (4): 75-84 (2017)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats., , , , , , and . USENIX Security Symposium, page 1465-1482. USENIX Association, (2019)Amber: Decoupling User Data from Web Applications., , , , , , and . HotOS, USENIX Association, (2015)Using Crash Hoare Logic for Certifying the FSCQ File System., , , , , and . USENIX Annual Technical Conference, USENIX Association, (2016)Using Crash Hoare logic for certifying the FSCQ file system., , , , , and . SOSP, page 18-37. ACM, (2015)Verifying a high-performance crash-safe file system using a tree specification., , , , , , , and . SOSP, page 270-286. ACM, (2017)Verifying concurrent software using movers in CSPEC., , , and . OSDI, page 306-322. USENIX Association, (2018)Certifying a file system using crash hoare logic: correctness in the presence of crashes., , , , , and . Commun. ACM, 60 (4): 75-84 (2017)Argosy: verifying layered storage systems with recovery refinement., , , and . PLDI, page 1054-1068. ACM, (2019)Proving confidentiality in a file system using DiskSec., , , , and . OSDI, page 323-338. USENIX Association, (2018)Natjam: design and evaluation of eviction policies for supporting priorities and deadlines in mapreduce clusters., , , , , , and . SoCC, page 6:1-6:17. ACM, (2013)