Persistency Semantics for Verification under Ext4
Working with files, one can observe weak behaviors: the kernel, the file system, and the hardware affect the order and atomicity of the file operations. Besides similar effects observed in memory, the persistency problem arises: In which state are the files observed upon a crash recovery? Being poorly documented, modern filesystems are hardly understood by programmers, which leads to severe software bugs, such as data corruption.
As a first step towards solving this problem, the formal model of the Linux ext4 has been proposed. In the talk, we’ll cover this model and the extension of GenMC model checker algorithm [1], enabling one to verify software performing file I/O. In addition, there will be presented several bugs in commonlyused text editors (such as vim and nano) revealed by the algorithm.
Speaker: Ilya Kaisin
[1] GenMC model checker http://plv.mpisws.org/genmc/
The seminar will be held in google meet on Monday September 21 at 17:30 (google meet room: https://meet.google.com/myudhmzgvu)
 About seminars

26 October 2020Representability of invariants of programs with algebraic data type

19 October 2020Stepindexing semantics of recursive types

12 October 2020Incorrectness Logic

5 October 2020Development of domainspecific compilers for specialized processors

28 September 2020Slightly subcubic algorithm for the contextfree language reachability (CFLreachability) problem