Gerhard Schellhorn

ORCID

Publication Activity (10 Years)

Years Active: 1993-2024
Publications (10 Years): 26

Top Venues

ABZ

IFM

CoRR

University of Ulm, Germany (PHD)

Education History

University of Ulm, Germany

PHD

Publications

Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
A Fully Verified Persistency Library. VMCAI (2) (2024)
Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif
Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems. ABZ (2023)
Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif
Refinement and Separation: Modular Verification of Wandering Trees. iFM (2023)
Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. CONCUR (2022)
Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich, Wolfgang Reif
Software & System Verification with KIV. The Logic of Software. A Tasting Menu of Formal Methods (2022)
Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Modularising Verification Of Durable Opacity. Log. Methods Comput. Sci. 18 (3) (2022)
Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich, Wolfgang Reif
Separating Separation Logic - Modular Verification of Red-Black Trees. VSTTE (2022)
Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
Verification of Crashsafe Caching in a Virtual File System Switch. Formal Aspects Comput. 34 (1) (2022)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput. 33 (4-5) (2021)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Brief Announcement: On Strong Observational Refinement and Forward Simulation. DISC (2021)
Stefan Bodenmüller, Gerhard Schellhorn, Martin Bitterlich, Wolfgang Reif
Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System. Logic, Computation and Rigorous Methods (2021)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
On Strong Observational Refinement and Forward Simulation. CoRR (2021)
Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. CoRR (2020)
Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. FORTE (2020)
Gerhard Schellhorn, Stefan Bodenmüller, Jörg Pfähler, Wolfgang Reif
Adding Concurrency to a Sequential Refinement Tower. ABZ (2020)
Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch. IFM (2020)
Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Modularising Verification Of Durable Opacity. CoRR (2020)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
Verifying Correctness of Persistent Concurrent Data Structures. FM (2019)
Gerhard Schellhorn, Monika Wedel, Oleg Travkin, Jürgen König, Heike Wehrheim
FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity. SEFM (2018)
Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller, Wolfgang Reif
Symbolic execution for a clash-free subset of ASMs. Sci. Comput. Program. 158 (2018)
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. 30 (5) (2018)
Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
Modular Verification of Order-Preserving Write-Back Caches. IFM (2017)
Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
A Relational Encoding for a Clash-Free Subset of ASMs. ABZ (2016)
Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
Modular, crash-safe refinement for ASMs with submachines. Sci. Comput. Program. 131 (2016)
Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
Proving Opacity of a Pessimistic STM. OPODIS (2016)
Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
Towards a Thread-Local Proof Technique for Starvation Freedom. IFM (2016)
Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
Inside a Verified Flash File System: Transactions and Garbage Collection. VSTTE (2015)
John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
Verifying Opacity of a Transactional Mutex Lock. FM (2015)
Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transf. 17 (6) (2015)
Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
trees by integration of shape analysis and interactive theorem proving. Softw. Syst. Model. 14 (1) (2015)
Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
Modular Refinement for Submachines of ASMs. ABZ (2014)
John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim
Quiescent Consistency: Defining and Verifying Relaxed Linearizability. FM (2014)
Gerhard Schellhorn, John Derrick, Heike Wehrheim
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. ACM Trans. Comput. Log. 15 (4) (2014)
Bogdan Tofan, Oleg Travkin, Gerhard Schellhorn, Heike Wehrheim
Two approaches for proving linearizability of multiset. Sci. Comput. Program. 96 (2014)
Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif
A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset. IFM (2014)
Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
RGITL: A temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. 71 (1-3) (2014)
Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif
Development of a Verified Flash File System. ABZ (2014)
Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
Compositional Verification of a Lock-Free Stack with RGITL. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013)
Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif
Verification of a Virtual Filesystem Switch. VSTTE (2013)
Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
Formal Specification of an Erase Block Management Layer for Flash Memory. Haifa Verification Conference (2013)
Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif
A Formal Model of a Virtual Filesystem Switch SSV (2012)
Oleg Travkin, Heike Wehrheim, Gerhard Schellhorn
Proving Linearizability of Multiset with Local Proof Obligations. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012)
Gerhard Schellhorn, Heike Wehrheim, John Derrick
How to Prove Algorithms Linearisable. CAV (2012)
Simon Bäumler, Gerhard Schellhorn, Bogdan Tofan, Wolfgang Reif
Proving linearizability with temporal logic. Formal Aspects Comput. 23 (1) (2011)
Dominik Haneberg, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
Mondex: Engineering a Provable Secure Electronic Purse. Int. J. Softw. Informatics 5 (1-2) (2011)
Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Wolfgang Reif
Interleaved Programs and Rely-Guarantee Reasoning with ITL. TIME (2011)
Gerhard Schellhorn
Completeness of fair ASM refinement. Sci. Comput. Program. 76 (9) (2011)
Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving. SEFM (2011)
John Derrick, Gerhard Schellhorn, Heike Wehrheim
Verifying Linearisability with Potential Linearisation Points. FM (2011)
John Derrick, Gerhard Schellhorn, Heike Wehrheim
Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33 (1) (2011)
Gerhard Schellhorn
Extending ITL with Interleaved Programs for Interactive Verification. TIME (2011)
Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif
Formal Verification of a Lock-Free Stack with Hazard Pointers. ICTAC (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
The COST IC0701 Verification Competition 2011. FoVeOOS (2011)
Eerke A. Boiten, John Derrick, Gerhard Schellhorn
Selected papers of the Refinement Workshop Turku (2008). Sci. Comput. Program. 76 (9) (2011)
Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst
Simulating a Flash File System with CoreASM and Eclipse. GI-Jahrestagung (2011)
Simon Bäumler, Michael Balser, Florian Nafz, Wolfgang Reif, Gerhard Schellhorn
Interactive verification of concurrent systems using symbolic execution. AI Commun. 23 (2-3) (2010)
Richard Banach, Gerhard Schellhorn
Atomic actions, and their refinements to isolated protocols. Formal Aspects Comput. 22 (1) (2010)
Bogdan Tofan, Simon Bäumler, Gerhard Schellhorn, Wolfgang Reif
Temporal Logic Verification of Lock-Freedom. MPC (2010)
Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
Automated Flaw Detection in Algebraic Specifications. J. Autom. Reason. 45 (4) (2010)
Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius, Wolfgang Reif
A Systematic Verification Approach for Mondex Electronic Purses Using ASMs. Rigorous Methods for Software Construction and Analysis (2009)
Eerke A. Boiten, John Derrick, Gerhard Schellhorn
Relational concurrent refinement part II: Internal operations and outputs. Formal Aspects Comput. 21 (1-2) (2009)
Gerhard Schellhorn, Simon Bäumler
Formal Verification of Lock-Free Algorithms. ACSD (2009)
Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
Abstract Specification of the UBIFS File System for Flash Memory. FM (2009)
John Derrick, Gerhard Schellhorn, Heike Wehrheim
Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack. FMOODS (2008)
Gerhard Schellhorn
Completeness of ASM Refinement. Electron. Notes Theor. Comput. Sci. 214 (2008)
Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
Automating Algebraic Specifications of Non-freely Generated Data Types. ATVA (2008)
Gerhard Schellhorn, Richard Banach
A Concept-Driven Construction of the Mondex Protocol Using Three Refinements. ABZ (2008)
Eerke A. Boiten, John Derrick, Gerhard Schellhorn
Preface. Electron. Notes Theor. Comput. Sci. 214 (2008)
Dominik Haneberg, Gerhard Schellhorn, Holger Grandy, Wolfgang Reif
Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Formal Aspects Comput. 20 (1) (2008)
Richard Banach, Gerhard Schellhorn
On the Refinement of Atomic Actions. Electron. Notes Theor. Comput. Sci. 201 (2008)
Gerhard Schellhorn
Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract). ABZ (2008)
Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
Bounded Relational Analysis of Free Data Types. TAP (2008)
Gerhard Schellhorn
ASM Refinement Preserving Invariants. J. Univers. Comput. Sci. 14 (12) (2008)
Holger Grandy, Markus Bischof, Kurt Stenzel, Gerhard Schellhorn, Wolfgang Reif
Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code. FM (2008)
Michael Balser, Simon Bäumler, Wolfgang Reif, Gerhard Schellhorn
Interactive Verification of Concurrent Systems using Symbolic Execution. LPAR Workshops (2008)
John Derrick, Gerhard Schellhorn, Heike Wehrheim
Proving Linearizability Via Non-atomic Refinement. IFM (2007)
Frank Ortmeier, Gerhard Schellhorn
Formal Fault Tree Analysis - Practical Experiences. Electron. Notes Theor. Comput. Sci. 185 (2007)
Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn
Verifying Smart Card Applications: An ASM Approach. IFM (2007)
Nina Moebius, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn
A Modeling Framework for the Development of Provably Secure E-Commerce Applications. ICSEA (2007)
Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif
The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. FM (2006)
Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn
Verifying Security Protocols: An ASM Approach. Abstract State Machines (2005)
Gerhard Schellhorn
ASMs and Refinement of State-based Systems. Abstract State Machines (2005)
Gerhard Schellhorn
ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor. Comput. Sci. 336 (2-3) (2005)
Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn
Formal Safety Analysis of a Radio-Based Railroad Crossing Using Deductive Cause-Consequence Analysis (DCCA). EDCC (2005)
Wolfgang Reif, Frank Ortmeier, Andreas Thums, Gerhard Schellhorn
Integrated formal methods for safety analysis of train systems. IFIP Congress Topical Sessions (2004)
Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn
Introduction to Subject Area "Verification". SoftSpez Final Report (2004)
Andreas Thums, Gerhard Schellhorn, Frank Ortmeier, Wolfgang Reif
Interactive Verification of Statecharts. SoftSpez Final Report (2004)
Frank Ortmeier, Andreas Thums, Gerhard Schellhorn, Wolfgang Reif
Combining Formal Methods and Safety Analysis - The ForMoSA Approach. SoftSpez Final Report (2004)
Rudolf Berghammer, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn
Special Issue on Tools for System Design and Verification. J. Univers. Comput. Sci. 9 (2) (2003)
Andreas Thums, Gerhard Schellhorn
Model Checking FTA. FME (2003)
Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering, Helmut Trappschuh
Safety analysis of the height control system for the Elbtunnel. Reliab. Eng. Syst. Saf. 81 (3) (2003)
Michael Balser, Christoph Duelli, Wolfgang Reif, Gerhard Schellhorn
Verifying Concurrent Systems with Symbolic Execution. J. Log. Comput. 12 (4) (2002)
Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering, Helmut Trappschuh
Safety Analysis of the Height Control System for the Elbtunnel. SAFECOMP (2002)
Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul A. Karger, Vernon Austel, David C. Toll
Verified Formal Security Models for Multiapplicative Smart Cards. J. Comput. Secur. 10 (4) (2002)
Wolfgang Reif, Gerhard Schellhorn
J.UCS Special Issue on Tools for System Design and Verification - Part 1. J. Univers. Comput. Sci. 7 (1) (2001)
Wolfgang Reif, Gerhard Schellhorn, Andreas Thums
Flaw Detection in Formal Specifications. IJCAR (2001)
Wolfgang Reif, Gerhard Schellhorn
J.UCS Special Issue on Tools for System Design and Verification - Part 2. J. Univers. Comput. Sci. 7 (2) (2001)
Gerhard Schellhorn
Verification of ASM Refinements Using Generalized Forward Simulation. J. Univers. Comput. Sci. 7 (11) (2001)
Wolfgang Reif, Gerhard Schellhorn, Tobias Vollmer, Jürgen Ruf
Correctness of Efficient Real-Time Model Checking. J. Univers. Comput. Sci. 7 (2) (2001)
Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Andreas Thums
Formal System Development with KIV. FASE (2000)

Gerhard Schellhorn.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Gerhard Schellhorn