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

• Part of GenMC @ Github

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++