Members of our research group participated in the VerifyThis competition at FM 2012 in
Paris using the interactive specification and verification system KIV. In this article we …

This paper gives an overview over the development of a formally verified file system for flash
memory. We describe our approach that is based on Abstract State Machines and …

The Flashix project has developed the first realistic verified file system for Flash memory.
This paper gives an overview over the project and the theory used. Specification is based on …

The work presented here addresses a long-standing conceptual gap in flash file system
verification: We map an abstract graph-based representation down to the flat blocks of bytes …

In this paper we define a formal refinement theory for a variant of Abstract State Machines
(ASMs) with submachines and power cuts. The theory is motivated by the development of a …

When developing file systems, caching is a common technique to achieve a performant
implementation. Integrating write-back caches is not primarily a problem for functional …

This paper defines a concept and a verification methodology for adding concurrency to a
sequential refinement tower of abstract state machines, that is based on data refinement and …

When developing file systems, caching is a common technique to achieve a performant
implementation. Integrating write-back caches into a file system does not only affect …

The main contribution of this thesis is a methodology for designing, implementing and
verifying realistic file systems with evidence of its effectiveness by application to a non-trivial …

Solid-state drives (SSDs) are fast emerging as the primary choice for data storage in diverse
domains. However, data protection against ransomware attacks on such storage devices is …