The KIV System: A Tool for Formal Program Development. - Rainer Drexler; Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel; Werner Stephan 001; Andreas Wolpers (STACS, 1993)

Formal Specification and Verification Using KIV. - Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (FTRTFT, 1994)

Tactics in KIV. - Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (J. Inf. Process. Cybern., 1994)

Three Selected Case Studies in Verification. - Thomas Fuchß; Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (KORSO Book, 1995)

KIV. - Gerhard Schellhorn; Axel Burandt (Formal Development of Reactive Systems, 1995)

Proving System Correctness with KIV 3.0. - Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (CADE, 1997)

Proving System Correctness with KIV. - Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (TAPSOFT, 1997)

Reasoning about Abstract State Machines: The WAM Case Study. - Gerhard Schellhorn; Wolfgang Ahrendt (J. Univers. Comput. Sci., 1997)

KIV 3.0 for Provably Correct Systems. - Michael Balser; Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (FM-Trends, 1998)

VSE: Controlling the Complexity in Formal Software Developments. - Dieter Hutter; Heiko Mantel; Georg Rock; Werner Stephan 001; Andreas Wolpers; Michael Balser; Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (FM-Trends, 1998)

Verifikation abstrakter Zustandsmaschinen. - Gerhard Schellhorn (1999)

Verification of a Formal Security Model for Multiapplicative Smart Cards. - Gerhard Schellhorn; Wolfgang Reif; Axel Schairer; Paul A. Karger; Vernon Austel; David C. Toll (ESORICS, 2000)

Formal System Development with KIV. - Michael Balser; Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel; Andreas Thums (FASE, 2000)

Do You Trust Your Model Checker? - Wolfgang Reif; Jürgen Ruf; Gerhard Schellhorn; Tobias Vollmer (FMCAD, 2000)

Flaw Detection in Formal Specifications. - Wolfgang Reif; Gerhard Schellhorn; Andreas Thums (IJCAR, 2001)

J.UCS Special Issue on Tools for System Design and Verification - Part 1. - Wolfgang Reif; Gerhard Schellhorn (J. Univers. Comput. Sci., 2001)

J.UCS Special Issue on Tools for System Design and Verification - Part 2. - Wolfgang Reif; Gerhard Schellhorn (J. Univers. Comput. Sci., 2001)

Correctness of Efficient Real-Time Model Checking. - Wolfgang Reif; Gerhard Schellhorn; Tobias Vollmer; Jürgen Ruf (J. Univers. Comput. Sci., 2001)

Verification of ASM Refinements Using Generalized Forward Simulation. - Gerhard Schellhorn (J. Univers. Comput. Sci., 2001)

Verified Formal Security Models for Multiapplicative Smart Cards. - Gerhard Schellhorn; Wolfgang Reif; Axel Schairer; Paul A. Karger; Vernon Austel; David C. Toll (J. Comput. Secur., 2002)

Verifying Concurrent Systems with Symbolic Execution. - Michael Balser; Christoph Duelli; Wolfgang Reif; Gerhard Schellhorn (J. Log. Comput., 2002)

Model Checking FTA. - Andreas Thums; Gerhard Schellhorn (FME, 2003)

Special Issue on Tools for System Design and Verification. - Rudolf Berghammer; Dominik Haneberg; Wolfgang Reif; Gerhard Schellhorn (J. Univers. Comput. Sci., 2003)

Safety analysis of the height control system for the Elbtunnel. - Frank Ortmeier; Gerhard Schellhorn; Andreas Thums; Wolfgang Reif; Bernhard Hering; Helmut Trappschuh (Reliab. Eng. Syst. Saf., 2003)

Introduction to Subject Area "Verification". - Frank Ortmeier; Wolfgang Reif; Gerhard Schellhorn (SoftSpez Final Report, 2004)

Combining Formal Methods and Safety Analysis - The ForMoSA Approach. - Frank Ortmeier; Andreas Thums; Gerhard Schellhorn; Wolfgang Reif (SoftSpez Final Report, 2004)

Interactive Verification of Statecharts. - Andreas Thums; Gerhard Schellhorn; Frank Ortmeier; Wolfgang Reif (SoftSpez Final Report, 2004)

Integrated formal methods for safety analysis of train systems. - Wolfgang Reif; Frank Ortmeier; Andreas Thums; Gerhard Schellhorn (IFIP Congress Topical Sessions, 2004)

Verifying Security Protocols: An ASM Approach. - Dominik Haneberg; Holger Grandy; Wolfgang Reif; Gerhard Schellhorn (Abstract State Machines, 2005)

ASMs and Refinement of State-based Systems. - Gerhard Schellhorn (Abstract State Machines, 2005)

Formal Safety Analysis of a Radio-Based Railroad Crossing Using Deductive Cause-Consequence Analysis (DCCA). - Frank Ortmeier; Wolfgang Reif; Gerhard Schellhorn (EDCC, 2005)

ASM refinement and generalizations of forward simulation in data refinement: a comparison. - Gerhard Schellhorn (Theor. Comput. Sci., 2005)

The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. - Gerhard Schellhorn; Holger Grandy; Dominik Haneberg; Wolfgang Reif (FM, 2006)

Formal Fault Tree Analysis - Practical Experiences. - Frank Ortmeier; Gerhard Schellhorn (AVoCS, 2006)

A Modeling Framework for the Development of Provably Secure E-Commerce Applications. - Nina Moebius; Dominik Haneberg; Wolfgang Reif; Gerhard Schellhorn (ICSEA, 2007)

Proving Linearizability Via Non-atomic Refinement. - John Derrick; Gerhard Schellhorn; Heike Wehrheim (IFM, 2007)

Verifying Smart Card Applications: An ASM Approach. - Dominik Haneberg; Holger Grandy; Wolfgang Reif; Gerhard Schellhorn (IFM, 2007)

On the Refinement of Atomic Actions. - Richard Banach; Gerhard Schellhorn (REFINE@IFM, 2007)

Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract). - Gerhard Schellhorn (ABZ, 2008)

A Concept-Driven Construction of the Mondex Protocol Using Three Refinements. - Gerhard Schellhorn; Richard Banach (ABZ, 2008)

Automating Algebraic Specifications of Non-freely Generated Data Types. - Andriy Dunets; Gerhard Schellhorn; Wolfgang Reif (ATVA, 2008)

Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code. - Holger Grandy; Markus Bischof; Kurt Stenzel; Gerhard Schellhorn; Wolfgang Reif (FM, 2008)

Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack. - John Derrick; Gerhard Schellhorn; Heike Wehrheim (FMOODS, 2008)

Interactive Verification of Concurrent Systems using Symbolic Execution. - Michael Balser; Simon Bäumler; Wolfgang Reif; Gerhard Schellhorn (LPAR Workshops, 2008)

Bounded Relational Analysis of Free Data Types. - Andriy Dunets; Gerhard Schellhorn; Wolfgang Reif (TAP, 2008)

Preface. - Eerke A. Boiten; John Derrick; Gerhard Schellhorn (Refine@FM, 2008)

Completeness of ASM Refinement. - Gerhard Schellhorn (Refine@FM, 2008)

Verification of Mondex electronic purses with KIV: from transactions to a security protocol. - Dominik Haneberg; Gerhard Schellhorn; Holger Grandy; Wolfgang Reif (Formal Aspects Comput., 2008)

ASM Refinement Preserving Invariants. - Gerhard Schellhorn (J. Univers. Comput. Sci., 2008)

Formal Verification of Lock-Free Algorithms. - Gerhard Schellhorn; Simon Bäumler (ACSD, 2009)

A Systematic Verification Approach for Mondex Electronic Purses Using ASMs. - Gerhard Schellhorn; Holger Grandy; Dominik Haneberg; Nina Moebius; Wolfgang Reif (Rigorous Methods for Software Construction and Analysis, 2009)

Abstract Specification of the UBIFS File System for Flash Memory. - Andreas Schierl; Gerhard Schellhorn; Dominik Haneberg; Wolfgang Reif (FM, 2009)

Relational concurrent refinement part II: Internal operations and outputs. - Eerke A. Boiten; John Derrick; Gerhard Schellhorn (Formal Aspects Comput., 2009)

Temporal Logic Verification of Lock-Freedom. - Bogdan Tofan; Simon Bäumler; Gerhard Schellhorn; Wolfgang Reif (MPC, 2010)

Interactive verification of concurrent systems using symbolic execution. - Simon Bäumler; Michael Balser; Florian Nafz; Wolfgang Reif; Gerhard Schellhorn (AI Commun., 2010)

Atomic actions, and their refinements to isolated protocols. - Richard Banach; Gerhard Schellhorn (Formal Aspects Comput., 2010)

Automated Flaw Detection in Algebraic Specifications. - Andriy Dunets; Gerhard Schellhorn; Wolfgang Reif (J. Autom. Reason., 2010)

Verifying Linearisability with Potential Linearisation Points. - John Derrick; Gerhard Schellhorn; Heike Wehrheim (FM, 2011)

The COST IC0701 Verification Competition 2011. - Thorsten Bormer; Marc Brockschmidt; Dino Distefano; Gidon Ernst; Jean-Christophe Filliâtre; Radu Grigore; Marieke Huisman; Vladimir Klebanov; Claude Marché; Rosemary Monahan; Wojciech Mostowski; Nadia Polikarpova; et al. (FoVeOOS, 2011)

Simulating a Flash File System with CoreASM and Eclipse. - Dominik Haneberg; Maximilian Junker; Gerhard Schellhorn; Wolfgang Reif; Gidon Ernst (GI-Jahrestagung, 2011)

Formal Verification of a Lock-Free Stack with Hazard Pointers. - Bogdan Tofan; Gerhard Schellhorn; Wolfgang Reif (ICTAC, 2011)

Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving. - Gidon Ernst; Gerhard Schellhorn; Wolfgang Reif (SEFM, 2011)

Extending ITL with Interleaved Programs for Interactive Verification. - Gerhard Schellhorn (TIME, 2011)

Interleaved Programs and Rely-Guarantee Reasoning with ITL. - Gerhard Schellhorn; Bogdan Tofan; Gidon Ernst; Wolfgang Reif (TIME, 2011)

Proving linearizability with temporal logic. - Simon Bäumler; Gerhard Schellhorn; Bogdan Tofan; Wolfgang Reif (Formal Aspects Comput., 2011)

Mondex: Engineering a Provable Secure Electronic Purse. - Dominik Haneberg; Nina Moebius; Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (Int. J. Softw. Informatics, 2011)

Selected papers of the Refinement Workshop Turku (2008). - Eerke A. Boiten; John Derrick; Gerhard Schellhorn (Sci. Comput. Program., 2011)

Completeness of fair ASM refinement. - Gerhard Schellhorn (Sci. Comput. Program., 2011)

Mechanically verified proof obligations for linearizability. - John Derrick; Gerhard Schellhorn; Heike Wehrheim (ACM Trans. Program. Lang. Syst., 2011)

How to Prove Algorithms Linearisable. - Gerhard Schellhorn; Heike Wehrheim; John Derrick (CAV, 2012)

A Formal Model of a Virtual Filesystem Switch - Gidon Ernst; Gerhard Schellhorn; Dominik Haneberg; Jörg Pfähler; Wolfgang Reif (SSV, 2012)

Proving Linearizability of Multiset with Local Proof Obligations. - Oleg Travkin; Heike Wehrheim; Gerhard Schellhorn (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

Formal Specification of an Erase Block Management Layer for Flash Memory. - Jörg Pfähler; Gidon Ernst; Gerhard Schellhorn; Dominik Haneberg; Wolfgang Reif (Haifa Verification Conference, 2013)

Verification of a Virtual Filesystem Switch. - Gidon Ernst; Gerhard Schellhorn; Dominik Haneberg; Jörg Pfähler; Wolfgang Reif (VSTTE, 2013)

Compositional Verification of a Lock-Free Stack with RGITL. - Bogdan Tofan; Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Wolfgang Reif (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Modular Refinement for Submachines of ASMs. - Gidon Ernst; Jörg Pfähler; Gerhard Schellhorn; Wolfgang Reif (ABZ, 2014)

Development of a Verified Flash File System. - Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Dominik Haneberg; Wolfgang Reif (ABZ, 2014)

Quiescent Consistency: Defining and Verifying Relaxed Linearizability. - John Derrick; Brijesh Dongol; Gerhard Schellhorn; Bogdan Tofan; Oleg Travkin; Heike Wehrheim (FM, 2014)

A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset. - Bogdan Tofan; Gerhard Schellhorn; Wolfgang Reif (IFM, 2014)

RGITL: A temporal logic framework for compositional reasoning about interleaved programs. - Gerhard Schellhorn; Bogdan Tofan; Gidon Ernst; Jörg Pfähler; Wolfgang Reif (Ann. Math. Artif. Intell., 2014)

Two approaches for proving linearizability of multiset. - Bogdan Tofan; Oleg Travkin; Gerhard Schellhorn; Heike Wehrheim (Sci. Comput. Program., 2014)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. - Gerhard Schellhorn; John Derrick; Heike Wehrheim (ACM Trans. Comput. Log., 2014)

Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications. - Marian Borek; Kuzman Katkalov; Nina Moebius; Wolfgang Reif; Gerhard Schellhorn; Kurt Stenzel (Correct Software in Web Applications and Web Services, 2015)

Verifying Opacity of a Transactional Mutex Lock. - John Derrick; Brijesh Dongol; Gerhard Schellhorn; Oleg Travkin; Heike Wehrheim (FM, 2015)

Inside a Verified Flash File System: Transactions and Garbage Collection. - Gidon Ernst; Jörg Pfähler; Gerhard Schellhorn; Wolfgang Reif (VSTTE, 2015)

Verification of B+ trees by integration of shape analysis and interactive theorem proving. - Gidon Ernst; Gerhard Schellhorn; Wolfgang Reif (Softw. Syst. Model., 2015)

KIV: overview and VerifyThis competition. - Gidon Ernst; Jörg Pfähler; Gerhard Schellhorn; Dominik Haneberg; Wolfgang Reif (Int. J. Softw. Tools Technol. Transf., 2015)

A Relational Encoding for a Clash-Free Subset of ASMs. - Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Wolfgang Reif (ABZ, 2016)

Towards a Thread-Local Proof Technique for Starvation Freedom. - Gerhard Schellhorn; Oleg Travkin; Heike Wehrheim (IFM, 2016)

Proving Opacity of a Pessimistic STM. - Simon Doherty; Brijesh Dongol; John Derrick; Gerhard Schellhorn; Heike Wehrheim (OPODIS, 2016)

Modular, crash-safe refinement for ASMs with submachines. - Gidon Ernst; Jörg Pfähler; Gerhard Schellhorn; Wolfgang Reif (Sci. Comput. Program., 2016)

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

FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity. - Gerhard Schellhorn; Monika Wedel; Oleg Travkin; Jürgen König; Heike Wehrheim (SEFM, 2018)

Mechanized proofs of opacity: a comparison of two techniques. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Oleg Travkin; Heike Wehrheim (Formal Aspects Comput., 2018)

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)

Verifying Correctness of Persistent Concurrent Data Structures. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (FM, 2019)

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

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. - Eleni Bila; Simon Doherty; Brijesh Dongol; John Derrick; Gerhard Schellhorn; Heike Wehrheim (FORTE, 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)

Brief Announcement: On Strong Observational Refinement and Forward Simulation. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (DISC, 2021)

On Strong Observational Refinement and Forward Simulation. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (CoRR, 2021)

Verifying correctness of persistent concurrent data structures: a sound and complete method. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (Formal Aspects Comput., 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)

Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. - Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (CONCUR, 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)

Modularising Verification Of Durable Opacity. - Eleni Bila; John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (Log. Methods Comput. Sci., 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)

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)

Eine REIFe Leistung - Anecdotes from Behind the Scenes. - Gidon Ernst; Dominik Haneberg; Matthias Güdemann; Oliver Kosak; Florian Nafz; Hella Ponsar; Gerhard Schellhorn (Go Where the Bugs Are, 2025)

A Tale of Formal Methods, Organic Computing, and Intelligent Robotics - The Scientific Life of Wolfgang Reif. - Dominik Haneberg; Alexander Knapp; Oliver Kosak; Florian Nafz; Hella Ponsar; Gerhard Schellhorn; Martin Wirsing (Go Where the Bugs Are, 2025)

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)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)