Gerhard Schellhorn

According to our database, Gerhard Schellhorn authored at least 113 papers between 1993 and 2025.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2025

Verification of forward simulations with thread-local, step-local proof obligations.

Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif

Sci. Comput. Program., 2025

2024

A Fully Verified Persistency Library.

Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2024

VeriCode: Correct Translation of Abstract Specifications to C Code.

Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif

Proceedings of the Integrated Formal Methods - 19th International Conference, 2024

2023

Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems.

Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif

Proceedings of the Rigorous State-Based Methods - 9th International Conference, 2023

Refinement and Separation: Modular Verification of Wandering Trees.

Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif

Proceedings of the iFM 2023 - 18th International Conference, 2023

2022

Modularising Verification Of Durable Opacity.

Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Log. Methods Comput. Sci., 2022

Verification of Crashsafe Caching in a Virtual File System Switch.

Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif

Formal Aspects Comput., 2022

Separating Separation Logic - Modular Verification of Red-Black Trees.

Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich, Wolfgang Reif

Proceedings of the Verified Software. Theories, Tools and Experiments, 2022

Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement.

Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the 33rd International Conference on Concurrency Theory, 2022

Software & System Verification with KIV.

Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich, Wolfgang Reif

Proceedings of the Logic of Software. A Tasting Menu of Formal Methods, 2022

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

On Strong Observational Refinement and Forward Simulation.

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

CoRR, 2021

Brief Announcement: On Strong Observational Refinement and Forward Simulation.

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the 35th International Symposium on Distributed Computing, 2021

Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System.

Stefan Bodenmüller, Gerhard Schellhorn, Martin Bitterlich, Wolfgang Reif

Proceedings of the Logic, Computation and Rigorous Methods, 2021

2020

Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch.

Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Integrated Formal Methods - 16th International Conference, 2020

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory.

Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2020

Adding Concurrency to a Sequential Refinement Tower.

Gerhard Schellhorn, Stefan Bodenmüller, Jörg Pfähler, Wolfgang Reif

Proceedings of the Rigorous State-Based Methods - 7th International Conference, 2020

2019

Verifying Correctness of Persistent Concurrent Data Structures.

John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

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

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

FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity.

Gerhard Schellhorn, Monika Wedel, Oleg Travkin, Jürgen König, Heike Wehrheim

Proceedings of the Software Engineering and Formal Methods - 16th International Conference, 2018

2017

Modular Verification of Order-Preserving Write-Back Caches.

Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Integrated Formal Methods - 13th International Conference, 2017

2016

Modular, crash-safe refinement for ASMs with submachines.

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif

Sci. Comput. Program., 2016

Proving Opacity of a Pessimistic STM.

Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the 20th International Conference on Principles of Distributed Systems, 2016

Towards a Thread-Local Proof Technique for Starvation Freedom.

Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim

Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

A Relational Encoding for a Clash-Free Subset of ASMs.

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

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

Verification of B⁺ trees by integration of shape analysis and interactive theorem proving.

Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif

Softw. Syst. Model., 2015

Inside a Verified Flash File System: Transactions and Garbage Collection.

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Verifying Opacity of a Transactional Mutex Lock.

John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim

Proceedings of the FM 2015: Formal Methods, 2015

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

Proceedings of the Correct Software in Web Applications and Web Services, 2015

2014

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures.

Gerhard Schellhorn, John Derrick, Heike Wehrheim

ACM Trans. Comput. Log., 2014

Two approaches for proving linearizability of multiset.

Bogdan Tofan, Oleg Travkin, Gerhard Schellhorn, Heike Wehrheim

Sci. Comput. Program., 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

A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset.

Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Quiescent Consistency: Defining and Verifying Relaxed Linearizability.

John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim

Proceedings of the FM 2014: Formal Methods, 2014

Development of a Verified Flash File System.

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

Modular Refinement for Submachines of ASMs.

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

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

Verification of a Virtual Filesystem Switch.

Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Formal Specification of an Erase Block Management Layer for Flash Memory.

Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif

Proceedings of the Hardware and Software: Verification and Testing, 2013

2012

Proving Linearizability of Multiset with Local Proof Obligations.

Oleg Travkin, Heike Wehrheim, Gerhard Schellhorn

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

A Formal Model of a Virtual Filesystem Switch

Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif

Proceedings of the Proceedings Seventh Conference on Systems Software Verification, 2012

How to Prove Algorithms Linearisable.

Gerhard Schellhorn, Heike Wehrheim, John Derrick

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Mechanically verified proof obligations for linearizability.

John Derrick, Gerhard Schellhorn, Heike Wehrheim

ACM Trans. Program. Lang. Syst., 2011

Completeness of fair ASM refinement.

Gerhard Schellhorn

Sci. Comput. Program., 2011

Selected papers of the Refinement Workshop Turku (2008).

Eerke A. Boiten, John Derrick, Gerhard Schellhorn

Sci. Comput. Program., 2011

Mondex: Engineering a Provable Secure Electronic Purse.

Dominik Haneberg, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

Int. J. Softw. Informatics, 2011

Proving linearizability with temporal logic.

Simon Bäumler, Gerhard Schellhorn, Bogdan Tofan, Wolfgang Reif

Formal Aspects Comput., 2011

Interleaved Programs and Rely-Guarantee Reasoning with ITL.

Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Wolfgang Reif

Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Extending ITL with Interleaved Programs for Interactive Verification.

Gerhard Schellhorn

Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving.

Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Software Engineering and Formal Methods - 9th International Conference, 2011

Formal Verification of a Lock-Free Stack with Hazard Pointers.

Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium, Johannesburg, South Africa, August 31, 2011

Simulating a Flash File System with CoreASM and Eclipse.

Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst

Proceedings of the 41. Jahrestagung der Gesellschaft für Informatik, 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, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, Mattias Ulbrich

Proceedings of the Formal Verification of Object-Oriented Software, 2011

Verifying Linearisability with Potential Linearisation Points.

John Derrick, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the FM 2011: Formal Methods, 2011

2010

Automated Flaw Detection in Algebraic Specifications.

Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif

J. Autom. Reason., 2010

Atomic actions, and their refinements to isolated protocols.

Richard Banach, Gerhard Schellhorn

Formal Aspects Comput., 2010

Interactive verification of concurrent systems using symbolic execution.

Simon Bäumler, Michael Balser, Florian Nafz, Wolfgang Reif, Gerhard Schellhorn

AI Commun., 2010

Temporal Logic Verification of Lock-Freedom.

Bogdan Tofan, Simon Bäumler, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010

2009

Relational concurrent refinement part II: Internal operations and outputs.

Eerke A. Boiten, John Derrick, Gerhard Schellhorn

Formal Aspects Comput., 2009

Abstract Specification of the UBIFS File System for Flash Memory.

Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif

Proceedings of the FM 2009: Formal Methods, 2009

A Systematic Verification Approach for Mondex Electronic Purses Using ASMs.

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius, Wolfgang Reif

Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009

Formal Verification of Lock-Free Algorithms.

Gerhard Schellhorn, Simon Bäumler

Proceedings of the Ninth International Conference on Application of Concurrency to System Design, 2009

2008

ASM Refinement Preserving Invariants.

Gerhard Schellhorn

J. Univers. Comput. Sci., 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

Completeness of ASM Refinement.

Gerhard Schellhorn

Proceedings of the 13th BAC-FACS Refinement Workshop, 2008

Preface.

Eerke A. Boiten, John Derrick, Gerhard Schellhorn

Proceedings of the 13th BAC-FACS Refinement Workshop, 2008

Bounded Relational Analysis of Free Data Types.

Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Tests and Proofs - 2nd International Conference, 2008

Interactive Verification of Concurrent Systems using Symbolic Execution.

Michael Balser, Simon Bäumler, Wolfgang Reif, Gerhard Schellhorn

Proceedings of the LPAR 2008 Workshops, 2008

Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack.

John Derrick, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 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

Proceedings of the FM 2008: Formal Methods, 2008

Automating Algebraic Specifications of Non-freely Generated Data Types.

Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Automated Technology for Verification and Analysis, 2008

A Concept-Driven Construction of the Mondex Protocol Using Three Refinements.

Gerhard Schellhorn, Richard Banach

Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract).

Gerhard Schellhorn

Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2007

On the Refinement of Atomic Actions.

Richard Banach, Gerhard Schellhorn

Proceedings of the BCS-FACS Refinement Workshop, 2007

Verifying Smart Card Applications: An ASM Approach.

Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn

Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Proving Linearizability Via Non-atomic Refinement.

John Derrick, Gerhard Schellhorn, Heike Wehrheim

Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

A Modeling Framework for the Development of Provably Secure E-Commerce Applications.

Nina Moebius, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn

Proceedings of the Second International Conference on Software Engineering Advances (ICSEA 2007), 2007

2006

Formal Fault Tree Analysis - Practical Experiences.

Frank Ortmeier, Gerhard Schellhorn

Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, 2006

The Mondex Challenge: Machine Checked Proofs for an Electronic Purse.

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif

Proceedings of the FM 2006: Formal Methods, 2006

2005

ASM refinement and generalizations of forward simulation in data refinement: a comparison.

Gerhard Schellhorn

Theor. Comput. Sci., 2005

Formal Safety Analysis of a Radio-Based Railroad Crossing Using Deductive Cause-Consequence Analysis (DCCA).

Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn

Proceedings of the Dependable Computing, 2005

ASMs and Refinement of State-based Systems.

Gerhard Schellhorn

Proceedings of the 12th International Workshop on Abstract State Machines, 2005

Verifying Security Protocols: An ASM Approach.

Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn

Proceedings of the 12th International Workshop on Abstract State Machines, 2005

2004

Integrated formal methods for safety analysis of train systems.

Wolfgang Reif, Frank Ortmeier, Andreas Thums, Gerhard Schellhorn

Proceedings of the Building the Information Society, 2004

Interactive Verification of Statecharts.

Andreas Thums, Gerhard Schellhorn, Frank Ortmeier, Wolfgang Reif

Proceedings of the Integration of Software Specification Techniques for Applications in Engineering, 2004

Combining Formal Methods and Safety Analysis - The ForMoSA Approach.

Frank Ortmeier, Andreas Thums, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Integration of Software Specification Techniques for Applications in Engineering, 2004

Introduction to Subject Area "Verification".

Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn

Proceedings of the Integration of Software Specification Techniques for Applications in Engineering, 2004

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

Special Issue on Tools for System Design and Verification.

Rudolf Berghammer, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn

J. Univers. Comput. Sci., 2003

Model Checking FTA.

Andreas Thums, Gerhard Schellhorn

Proceedings of the FME 2003: Formal Methods, 2003

2002

Verifying Concurrent Systems with Symbolic Execution.

Michael Balser, Christoph Duelli, Wolfgang Reif, Gerhard Schellhorn

J. Log. Comput., 2002

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

2001

Verification of ASM Refinements Using Generalized Forward Simulation.

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

J.UCS Special Issue on Tools for System Design and Verification - Part 2.

Wolfgang Reif, Gerhard Schellhorn

J. Univers. Comput. Sci., 2001

J.UCS Special Issue on Tools for System Design and Verification - Part 1.

Wolfgang Reif, Gerhard Schellhorn

J. Univers. Comput. Sci., 2001

Flaw Detection in Formal Specifications.

Wolfgang Reif, Gerhard Schellhorn, Andreas Thums

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

Do You Trust Your Model Checker?

Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn, Tobias Vollmer

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Formal System Development with KIV.

Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Andreas Thums

Proceedings of the Fundamental Approaches to Software Engineering, 2000

Verification of a Formal Security Model for Multiapplicative Smart Cards.

Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul A. Karger, Vernon Austel, David C. Toll

Proceedings of the Computer Security, 2000

1999

Verifikation abstrakter Zustandsmaschinen.

Gerhard Schellhorn

PhD thesis, 1999

1998

VSE: Controlling the Complexity in Formal Software Developments.

Dieter Hutter, Heiko Mantel, Georg Rock, Werner Stephan, Andreas Wolpers, Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

Proceedings of the Applied Formal Methods, 1998

KIV 3.0 for Provably Correct Systems.

Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

Proceedings of the Applied Formal Methods, 1998

1997

Reasoning about Abstract State Machines: The WAM Case Study.

Gerhard Schellhorn, Wolfgang Ahrendt

J. Univers. Comput. Sci., 1997

Proving System Correctness with KIV.

Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

Proving System Correctness with KIV 3.0.

Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

Proceedings of the Automated Deduction, 1997

1995

KIV.

Gerhard Schellhorn, Axel Burandt

Proceedings of the Formal Development of Reactive Systems - Case Study Production Cell, 1995

Three Selected Case Studies in Verification.

Thomas Fuchß, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

Proceedings of the KORSO, 1995

1994

Tactics in KIV.

Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

J. Inf. Process. Cybern., 1994

Formal Specification and Verification Using KIV.

Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

1993

The KIV System: A Tool for Formal Program Development.

Rainer Drexler, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Werner Stephan, Andreas Wolpers

Proceedings of the STACS 93, 1993