PerSeVerE: Persistency Semantics for Verification under Ext4
Summary
PerSeVerE is a framework encompassing (a) formal semantics for the Linux ext4 filesystem (which we integrate with the weak memory consistency semantics of C/C++), and (b) an effective model checking approach for verifying programs that use the filesystem. Using PerSeVerE, we were able to discover and report bugs in commonly-used text editors such as vim, emacs and nano.
Paper
-
PerSeVerE: Persistency Semantics for Verification under Ext4.
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis.
In POPL 2021 (To Appear)
[Pre-print (26 pages)] [@ACM] [Full paper with the technical appendix (33 pages)] [Artifact @Zenodo]
Implementation
People
- Michalis Kokologiannakis (MPI-SWS)
- Ilya Kaysin (National Research University Higher School of Economics, JetBrains Research)
- Azalea Raad (Imperial College London)
- Viktor Vafeiadis (MPI-SWS)
Related projects
- GenMC: a generic model checker for C/C++