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

Implementation

People

Related projects

Imprint | Data protection