@article{persevere,
author = {Kokologiannakis, Michalis and Kaysin, Ilya and Raad, Azalea and Vafeiadis, Viktor},
title = {PerSeVerE: Persistency Semantics for Verification under Ext4},
year = {2021},
issue_date = {January 2021},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {5},
number = {POPL},
url = {https://doi.org/10.1145/3434324},
doi = {10.1145/3434324},
abstract = {Although ubiquitous, modern filesystems have rather complex behaviours that are hardly understood by programmers and lead to severe software bugs such as data corruption. As a first step to ensure correctness of software performing file I/O, we formalize the semantics of the Linux ext4 filesystem, which we integrate with the weak memory consistency semantics of C/C++. We further develop an effective model checking approach for verifying programs that use the filesystem. In doing so, we discover and report bugs in commonly-used text editors such as vim, emacs and nano.},
journal = {Proc. ACM Program. Lang.},
month = {jan},
articleno = {43},
numpages = {29},
keywords = {Persistency, Weak Consistency, File Systems, Model Checking}
}