Name
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.
|
Year | DOI | Venue |
|---|---|---|
2021 | 10.1145/3434324 | Proceedings of the ACM on Programming Languages |
Keywords | DocType | Volume |
File Systems,Model Checking,Persistency,Weak Consistency | Journal | 5 |
Issue | ISSN | Citations |
POPL | 2475-1421 | 1 |
PageRank | References | Authors |
0.37 | 0 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michalis Kokologiannakis | 1 | 4 | 2.16 |
| Ilya Kaysin | 2 | 1 | 0.37 |
| Azalea Raad | 3 | 40 | 6.42 |
| Viktor Vafeiadis | 4 | 942 | 47.11 |