Gerhard Schellhorn

122 papers A* 1A 5B 25C 13Misc 1Journal 39Unranked 32

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	A Tale of Formal Methods, Organic Computing, and Intelligent Robotics - The Scientific Life of Wolfgang Reif. Go Where the Bugs Are Dominik Haneberg, Alexander Knapp, Oliver Kosak, Florian Nafz, Hella Ponsar, Gerhard Schellhorn, Martin Wirsing
2025	—	`conf`	Eine REIFe Leistung - Anecdotes from Behind the Scenes. Go Where the Bugs Are Gidon Ernst, Dominik Haneberg, Matthias Güdemann, Oliver Kosak, Florian Nafz, Hella Ponsar, Gerhard Schellhorn
2025	—	`ed.`	Go Where the Bugs Are - Essays Dedicated to Wolfgang Reif on the Occasion of His 65th Birthday Go Where the Bugs Are Gidon Ernst, Matthias Güdemann, Alexander Knapp, Florian Nafz, Frank Ortmeier, Hella Ponsar, Gerhard Schellhorn, Alexander Schiendorfer
2025	—	`conf`	Mirror is Not Strong: Discovery of a Persistent Memory Bug using Refinement in KIV. Go Where the Bugs Are Gerhard Schellhorn, Stefan Bodenmüller, Brijesh Dongol, Heike Wehrheim
2025	B	`conf`	Model Checking Buffered Durable Linearizability in CSP. iFM Chelsea Edmonds, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2025	J	`jnl`	Verification of forward simulations with thread-local, step-local proof obligations. Sci. Comput. Program. Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif
2024	—	`conf`	A Fully Verified Persistency Library. VMCAI (2) Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2024	B	`conf`	VeriCode: Correct Translation of Abstract Specifications to C Code. IFM Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif
2023	B	`conf`	Refinement and Separation: Modular Verification of Wandering Trees. iFM Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif
2023	C	`conf`	Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems. ABZ Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif
2022	J	`jnl`	Modularising Verification Of Durable Opacity. Log. Methods Comput. Sci. Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2022	—	`conf`	Separating Separation Logic - Modular Verification of Red-Black Trees. VSTTE Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich, Wolfgang Reif
2022	—	`conf`	Software & System Verification with KIV. The Logic of Software. A Tasting Menu of Formal Methods Gerhard Schellhorn, Stefan Bodenmüller, Martin Bitterlich, Wolfgang Reif
2022	J	`jnl`	Verification of Crashsafe Caching in a Virtual File System Switch. Formal Aspects Comput. Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
2022	B	`conf`	Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. CONCUR Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2021	A	`conf`	Brief Announcement: On Strong Observational Refinement and Forward Simulation. DISC John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2021	—	`conf`	Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System. Logic, Computation and Rigorous Methods Stefan Bodenmüller, Gerhard Schellhorn, Martin Bitterlich, Wolfgang Reif
2021	J	`jnl`	On Strong Observational Refinement and Forward Simulation. CoRR John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2021	J	`jnl`	Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput. John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2020	C	`conf`	Adding Concurrency to a Sequential Refinement Tower. ABZ Gerhard Schellhorn, Stefan Bodenmüller, Jörg Pfähler, Wolfgang Reif
2020	C	`conf`	Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. FORTE Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
2020	J	`jnl`	Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. CoRR Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
2020	B	`conf`	Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch. IFM Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
2020	J	`jnl`	Modularising Verification Of Durable Opacity. CoRR Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2019	B	`conf`	Verifying Correctness of Persistent Concurrent Data Structures. FM John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2018	B	`conf`	FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity. SEFM Gerhard Schellhorn, Monika Wedel, Oleg Travkin, Jürgen König, Heike Wehrheim
2018	J	`jnl`	Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
2018	J	`jnl`	Symbolic execution for a clash-free subset of ASMs. Sci. Comput. Program. Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller, Wolfgang Reif
2017	B	`conf`	Modular Verification of Order-Preserving Write-Back Caches. IFM Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
2016	C	`conf`	A Relational Encoding for a Clash-Free Subset of ASMs. ABZ Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
2016	J	`jnl`	Modular, crash-safe refinement for ASMs with submachines. Sci. Comput. Program. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
2016	B	`conf`	Proving Opacity of a Pessimistic STM. OPODIS Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
2016	B	`conf`	Towards a Thread-Local Proof Technique for Starvation Freedom. IFM Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
2015	—	`conf`	Inside a Verified Flash File System: Transactions and Garbage Collection. VSTTE Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
2015	—	`ch.`	Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications. Correct Software in Web Applications and Web Services Marian Borek, Kuzman Katkalov, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
2015	J	`jnl`	KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transf. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
2015	J	`jnl`	Verification of B Softw. Syst. Model. Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
2015	B	`conf`	Verifying Opacity of a Transactional Mutex Lock. FM John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
2014	B	`conf`	A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset. IFM Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif
2014	J	`jnl`	A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. ACM Trans. Comput. Log. Gerhard Schellhorn, John Derrick, Heike Wehrheim
2014	C	`conf`	Development of a Verified Flash File System. ABZ Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif
2014	C	`conf`	Modular Refinement for Submachines of ASMs. ABZ Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
2014	B	`conf`	Quiescent Consistency: Defining and Verifying Relaxed Linearizability. FM John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim
2014	J	`jnl`	RGITL: A temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
2014	J	`jnl`	Two approaches for proving linearizability of multiset. Sci. Comput. Program. Bogdan Tofan, Oleg Travkin, Gerhard Schellhorn, Heike Wehrheim
2013	J	`jnl`	Compositional Verification of a Lock-Free Stack with RGITL. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
2013	—	`conf`	Formal Specification of an Erase Block Management Layer for Flash Memory. Haifa Verification Conference Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
2013	—	`conf`	Verification of a Virtual Filesystem Switch. VSTTE Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif
2012	—	`conf`	A Formal Model of a Virtual Filesystem Switch SSV Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif
2012	A*	`conf`	How to Prove Algorithms Linearisable. CAV Gerhard Schellhorn, Heike Wehrheim, John Derrick
2012	J	`jnl`	Proving Linearizability of Multiset with Local Proof Obligations. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Oleg Travkin, Heike Wehrheim, Gerhard Schellhorn
2011	J	`jnl`	Completeness of fair ASM refinement. Sci. Comput. Program. Gerhard Schellhorn
2011	C	`conf`	Extending ITL with Interleaved Programs for Interactive Verification. TIME Gerhard Schellhorn
2011	C	`conf`	Formal Verification of a Lock-Free Stack with Hazard Pointers. ICTAC Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif
2011	C	`conf`	Interleaved Programs and Rely-Guarantee Reasoning with ITL. TIME Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Wolfgang Reif
2011	J	`jnl`	Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. John Derrick, Gerhard Schellhorn, Heike Wehrheim
2011	J	`jnl`	Mondex: Engineering a Provable Secure Electronic Purse. Int. J. Softw. Informatics Dominik Haneberg, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
2011	J	`jnl`	Proving linearizability with temporal logic. Formal Aspects Comput. Simon Bäumler, Gerhard Schellhorn, Bogdan Tofan, Wolfgang Reif
2011	J	`jnl`	Selected papers of the Refinement Workshop Turku (2008). Sci. Comput. Program. Eerke A. Boiten, John Derrick, Gerhard Schellhorn
2011	—	`conf`	Simulating a Flash File System with CoreASM and Eclipse. GI-Jahrestagung Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst
2011	—	`conf`	The COST IC0701 Verification Competition 2011. FoVeOOS 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
2011	B	`conf`	Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving. SEFM Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
2011	B	`conf`	Verifying Linearisability with Potential Linearisation Points. FM John Derrick, Gerhard Schellhorn, Heike Wehrheim
2010	J	`jnl`	Atomic actions, and their refinements to isolated protocols. Formal Aspects Comput. Richard Banach, Gerhard Schellhorn
2010	J	`jnl`	Automated Flaw Detection in Algebraic Specifications. J. Autom. Reason. Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
2010	J	`jnl`	Interactive verification of concurrent systems using symbolic execution. AI Commun. Simon Bäumler, Michael Balser, Florian Nafz, Wolfgang Reif, Gerhard Schellhorn
2010	B	`conf`	Temporal Logic Verification of Lock-Freedom. MPC Bogdan Tofan, Simon Bäumler, Gerhard Schellhorn, Wolfgang Reif
2009	—	`conf`	A Systematic Verification Approach for Mondex Electronic Purses Using ASMs. Rigorous Methods for Software Construction and Analysis Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius, Wolfgang Reif
2009	B	`conf`	Abstract Specification of the UBIFS File System for Flash Memory. FM Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
2009	—	`conf`	Formal Verification of Lock-Free Algorithms. ACSD Gerhard Schellhorn, Simon Bäumler
2009	J	`jnl`	Relational concurrent refinement part II: Internal operations and outputs. Formal Aspects Comput. Eerke A. Boiten, John Derrick, Gerhard Schellhorn
2008	C	`conf`	A Concept-Driven Construction of the Mondex Protocol Using Three Refinements. ABZ Gerhard Schellhorn, Richard Banach
2008	J	`jnl`	ASM Refinement Preserving Invariants. J. Univers. Comput. Sci. Gerhard Schellhorn
2008	B	`conf`	Automating Algebraic Specifications of Non-freely Generated Data Types. ATVA Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
2008	C	`conf`	Bounded Relational Analysis of Free Data Types. TAP Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
2008	—	`conf`	Completeness of ASM Refinement. Refine@FM Gerhard Schellhorn
2008	—	`conf`	Interactive Verification of Concurrent Systems using Symbolic Execution. LPAR Workshops Michael Balser, Simon Bäumler, Wolfgang Reif, Gerhard Schellhorn
2008	—	`conf`	Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack. FMOODS John Derrick, Gerhard Schellhorn, Heike Wehrheim
2008	—	`conf`	Preface. Refine@FM Eerke A. Boiten, John Derrick, Gerhard Schellhorn
2008	—	`ed.`	Proceedings of the 13th BAC-FACS Refinement Workshop, Refine@FM 2008, Turku, Finland, May 27, 2008 Refine@FM Eerke A. Boiten, John Derrick, Gerhard Schellhorn
2008	C	`conf`	Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract). ABZ Gerhard Schellhorn
2008	B	`conf`	Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code. FM Holger Grandy, Markus Bischof, Kurt Stenzel, Gerhard Schellhorn, Wolfgang Reif
2008	J	`jnl`	Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Formal Aspects Comput. Dominik Haneberg, Gerhard Schellhorn, Holger Grandy, Wolfgang Reif
2007	C	`conf`	A Modeling Framework for the Development of Provably Secure E-Commerce Applications. ICSEA Nina Moebius, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn
2007	—	`conf`	On the Refinement of Atomic Actions. REFINE@IFM Richard Banach, Gerhard Schellhorn
2007	B	`conf`	Proving Linearizability Via Non-atomic Refinement. IFM John Derrick, Gerhard Schellhorn, Heike Wehrheim
2007	B	`conf`	Verifying Smart Card Applications: An ASM Approach. IFM Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn
2006	—	`conf`	Formal Fault Tree Analysis - Practical Experiences. AVoCS Frank Ortmeier, Gerhard Schellhorn
2006	B	`conf`	The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. FM Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif
2005	J	`jnl`	ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor. Comput. Sci. Gerhard Schellhorn
2005	—	`conf`	ASMs and Refinement of State-based Systems. Abstract State Machines Gerhard Schellhorn
2005	Misc	`conf`	Formal Safety Analysis of a Radio-Based Railroad Crossing Using Deductive Cause-Consequence Analysis (DCCA). EDCC Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn
2005	—	`conf`	Verifying Security Protocols: An ASM Approach. Abstract State Machines Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn
2004	—	`conf`	Combining Formal Methods and Safety Analysis - The ForMoSA Approach. SoftSpez Final Report Frank Ortmeier, Andreas Thums, Gerhard Schellhorn, Wolfgang Reif
2004	—	`conf`	Integrated formal methods for safety analysis of train systems. IFIP Congress Topical Sessions Wolfgang Reif, Frank Ortmeier, Andreas Thums, Gerhard Schellhorn
2004	—	`conf`	Interactive Verification of Statecharts. SoftSpez Final Report Andreas Thums, Gerhard Schellhorn, Frank Ortmeier, Wolfgang Reif
2004	—	`conf`	Introduction to Subject Area "Verification". SoftSpez Final Report Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn
2003	—	`conf`	Model Checking FTA. FME Andreas Thums, Gerhard Schellhorn
2003	J	`jnl`	Safety analysis of the height control system for the Elbtunnel. Reliab. Eng. Syst. Saf. Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering, Helmut Trappschuh
2003	J	`jnl`	Special Issue on Tools for System Design and Verification. J. Univers. Comput. Sci. Rudolf Berghammer, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn
2002	B	`conf`	Safety Analysis of the Height Control System for the Elbtunnel. SAFECOMP Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering, Helmut Trappschuh
2002	J	`jnl`	Verified Formal Security Models for Multiapplicative Smart Cards. J. Comput. Secur. Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul A. Karger, Vernon Austel, David C. Toll
2002	J	`jnl`	Verifying Concurrent Systems with Symbolic Execution. J. Log. Comput. Michael Balser, Christoph Duelli, Wolfgang Reif, Gerhard Schellhorn
2001	J	`jnl`	Correctness of Efficient Real-Time Model Checking. J. Univers. Comput. Sci. Wolfgang Reif, Gerhard Schellhorn, Tobias Vollmer, Jürgen Ruf
2001	A	`conf`	Flaw Detection in Formal Specifications. IJCAR Wolfgang Reif, Gerhard Schellhorn, Andreas Thums
2001	J	`jnl`	J.UCS Special Issue on Tools for System Design and Verification - Part 1. J. Univers. Comput. Sci. Wolfgang Reif, Gerhard Schellhorn
2001	J	`jnl`	J.UCS Special Issue on Tools for System Design and Verification - Part 2. J. Univers. Comput. Sci. Wolfgang Reif, Gerhard Schellhorn
2001	J	`jnl`	Verification of ASM Refinements Using Generalized Forward Simulation. J. Univers. Comput. Sci. Gerhard Schellhorn
2000	B	`conf`	Do You Trust Your Model Checker? FMCAD Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn, Tobias Vollmer
2000	B	`conf`	Formal System Development with KIV. FASE Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Andreas Thums
2000	A	`conf`	Verification of a Formal Security Model for Multiapplicative Smart Cards. ESORICS Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul A. Karger, Vernon Austel, David C. Toll
1999	—	`—`	Verifikation abstrakter Zustandsmaschinen. Gerhard Schellhorn
1998	—	`conf`	KIV 3.0 for Provably Correct Systems. FM-Trends Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1998	—	`conf`	VSE: Controlling the Complexity in Formal Software Developments. FM-Trends Dieter Hutter, Heiko Mantel, Georg Rock, Werner Stephan, Andreas Wolpers, Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1997	A	`conf`	Proving System Correctness with KIV 3.0. CADE Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1997	—	`conf`	Proving System Correctness with KIV. TAPSOFT Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1997	J	`jnl`	Reasoning about Abstract State Machines: The WAM Case Study. J. Univers. Comput. Sci. Gerhard Schellhorn, Wolfgang Ahrendt
1995	—	`ch.`	KIV. Formal Development of Reactive Systems Gerhard Schellhorn, Axel Burandt
1995	—	`ch.`	Three Selected Case Studies in Verification. KORSO Book Thomas Fuchß, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1994	—	`conf`	Formal Specification and Verification Using KIV. FTRTFT Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1994	J	`jnl`	Tactics in KIV. J. Inf. Process. Cybern. Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1993	A	`conf`	The KIV System: A Tool for Formal Program Development. STACS Rainer Drexler, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Werner Stephan, Andreas Wolpers