DFG is funding the second Phase of Flashix

We are glad, that the DFG has recently announced to fund our research project "Flashix - Verification of Flash File Systems" for a second phase of two years. The project is lead by Prof. Dr. Wolfgang Reif.

The aim of the Flashix project is the full-scale verification of a flash file system. Flash memory is by now the dominant technology for mobile and embedded systems. It is faster, more energy-efficient and shock-resistant than traditional memory. However, its efficient use and life span are highly dependent upon complex algorithms, posing a challenge for state-of-the-art verification technology. The first phase of the Flashix project demonstrated that known and new techniques in the context of refinement hierarchies can be employed to tackle this challenge. However, robustness against system crashes, concurrency and non-local performance optimizations reach the practical limitations of a modular verification with refinement hierarchies. In the follow- up project we therefore develop an extension to facilitate a modular and incremental verification of non-local refinements in hierarchical systems, which can overcome these limitations. The problems are not limited to flash filesystems, but can be found in many embedded and performance-critical systems. The new verification technique is applied to the Flashix file system, completing its verification. The result is a fully verified file system for flash memory, that efficiently implements the POSIX standard in C and is deployable in practice.


message of 06.04.2016