Modular Verification of Order-Preserving Write-Back Caches. - Jörg Pfähler; Gidon Ernst; Stefan Bodenmüller; Gerhard Schellhorn; Wolfgang Reif (IFM, 2017)

Symbolic execution for a clash-free subset of ASMs. - Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Stefan Bodenmüller; Wolfgang Reif (Sci. Comput. Program., 2018)

Adding Concurrency to a Sequential Refinement Tower. - Gerhard Schellhorn; Stefan Bodenmüller; Jörg Pfähler; Wolfgang Reif (ABZ, 2020)

Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch. - Stefan Bodenmüller; Gerhard Schellhorn; Wolfgang Reif (IFM, 2020)

Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System. - Stefan Bodenmüller; Gerhard Schellhorn; Martin Bitterlich; Wolfgang Reif (Logic, Computation and Rigorous Methods, 2021)

Software & System Verification with KIV. - Gerhard Schellhorn; Stefan Bodenmüller; Martin Bitterlich; Wolfgang Reif (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

Separating Separation Logic - Modular Verification of Red-Black Trees. - Gerhard Schellhorn; Stefan Bodenmüller; Martin Bitterlich; Wolfgang Reif (VSTTE, 2022)

Verification of Crashsafe Caching in a Virtual File System Switch. - Stefan Bodenmüller; Gerhard Schellhorn; Wolfgang Reif (Formal Aspects Comput., 2022)

Refinement and Separation: Modular Verification of Wandering Trees. - Gerhard Schellhorn; Stefan Bodenmüller; Wolfgang Reif (iFM, 2023)

Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems. - Gerhard Schellhorn; Stefan Bodenmüller; Wolfgang Reif (ABZ, 2023)

Caching, crashing & concurrency - verification under adverse conditions. - Stefan Bodenmüller (2023)

VeriCode: Correct Translation of Abstract Specifications to C Code. - Gerhard Schellhorn; Stefan Bodenmüller; Wolfgang Reif (IFM, 2024)

A Fully Verified Persistency Library. - Stefan Bodenmüller; John Derrick; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (VMCAI (2), 2024)

Mirror is Not Strong: Discovery of a Persistent Memory Bug using Refinement in KIV. - Gerhard Schellhorn; Stefan Bodenmüller; Brijesh Dongol; Heike Wehrheim (Go Where the Bugs Are, 2025)

Verification of forward simulations with thread-local, step-local proof obligations. - Gerhard Schellhorn; Stefan Bodenmüller; Wolfgang Reif (Sci. Comput. Program., 2025)