default search action
Gerhard Schellhorn
Person information
- affiliation: University of Augsburg, Department of Computer Science, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2025
- [j36]Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif:
Verification of forward simulations with thread-local, step-local proof obligations. Sci. Comput. Program. 241: 103227 (2025) - 2024
- [c73]Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif:
VeriCode: Correct Translation of Abstract Specifications to C Code. IFM 2024: 53-74 - [c72]Stefan Bodenmüller
, John Derrick
A Fully Verified Persistency Library. VMCAI (2) 2024: 26-47 - 2023
- [c71]Gerhard Schellhorn
Refinement and Separation: Modular Verification of Wandering Trees. iFM 2023: 214-234 - [c70]Gerhard Schellhorn, Stefan Bodenmüller
Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems. ABZ 2023: 70-87 - 2022
- [j35]Stefan Bodenmüller
Verification of Crashsafe Caching in a Virtual File System Switch. Formal Aspects Comput. 34(1): 1-33 (2022) - [j34]Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol
Modularising Verification Of Durable Opacity. Log. Methods Comput. Sci. 18(3) (2022) - [c69]Gerhard Schellhorn, Stefan Bodenmüller
Software & System Verification with KIV. The Logic of Software. A Tasting Menu of Formal Methods 2022: 408-436 - [c68]Brijesh Dongol
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. CONCUR 2022: 31:1-31:23 - [c67]Gerhard Schellhorn, Stefan Bodenmüller
Separating Separation Logic - Modular Verification of Red-Black Trees. VSTTE 2022: 129-147 - 2021
- [j33]John Derrick, Simon Doherty, Brijesh Dongol
Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput. 33(4-5): 547-573 (2021) - [c66]Stefan Bodenmüller
Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System. Logic, Computation and Rigorous Methods 2021: 239-265 - [c65]John Derrick
Brief Announcement: On Strong Observational Refinement and Forward Simulation. DISC 2021: 55:1-55:4 - [i3]John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
On Strong Observational Refinement and Forward Simulation. CoRR abs/2107.14509 (2021) - 2020
- [c64]Gerhard Schellhorn, Stefan Bodenmüller
Adding Concurrency to a Sequential Refinement Tower. ABZ 2020: 6-23 - [c63]Eleni Bila, Simon Doherty, Brijesh Dongol
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. FORTE 2020: 39-58 - [c62]Stefan Bodenmüller
Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch. IFM 2020: 218-236 - [i2]Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim:
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. CoRR abs/2004.08200 (2020) - [i1]Eleni Bila, John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
Modularising Verification Of Durable Opacity. CoRR abs/2011.15013 (2020)
2010 – 2019
- 2019
- [c61]John Derrick
Verifying Correctness of Persistent Concurrent Data Structures. FM 2019: 179-195 - 2018
- [j32]John Derrick
Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. 30(5): 597-625 (2018) - [j31]Gerhard Schellhorn, Gidon Ernst
Symbolic execution for a clash-free subset of ASMs. Sci. Comput. Program. 158: 21-40 (2018) - [c60]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: 105-120 - 2017
- [c59]Jörg Pfähler, Gidon Ernst
Modular Verification of Order-Preserving Write-Back Caches. IFM 2017: 375-390 - 2016
- [j30]Gidon Ernst
Modular, crash-safe refinement for ASMs with submachines. Sci. Comput. Program. 131: 3-21 (2016) - [c58]Gerhard Schellhorn, Gidon Ernst
A Relational Encoding for a Clash-Free Subset of ASMs. ABZ 2016: 237-243 - [c57]Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim:
Towards a Thread-Local Proof Technique for Starvation Freedom. IFM 2016: 193-209 - [c56]Simon Doherty, Brijesh Dongol
Proving Opacity of a Pessimistic STM. OPODIS 2016: 35:1-35:17 - 2015
- [j29]Gidon Ernst
Verification of B+ trees by integration of shape analysis and interactive theorem proving. Softw. Syst. Model. 14(1): 27-44 (2015) - [j28]Gidon Ernst
KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transf. 17(6): 677-694 (2015) - [c55]John Derrick
Verifying Opacity of a Transactional Mutex Lock. FM 2015: 161-177 - [c54]Gidon Ernst
Inside a Verified Flash File System: Transactions and Garbage Collection. VSTTE 2015: 73-93 - [p3]Marian Borek, Kuzman Katkalov, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel:
Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications. Correct Software in Web Applications and Web Services 2015: 45-81 - 2014
- [j27]Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst
RGITL: A temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. 71(1-3): 131-174 (2014) - [j26]Bogdan Tofan, Oleg Travkin, Gerhard Schellhorn, Heike Wehrheim:
Two approaches for proving linearizability of multiset. Sci. Comput. Program. 96: 297-314 (2014) - [j25]Gerhard Schellhorn, John Derrick
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. ACM Trans. Comput. Log. 15(4): 31:1-31:37 (2014) - [c53]Gerhard Schellhorn, Gidon Ernst
Development of a Verified Flash File System. ABZ 2014: 9-24 - [c52]Gidon Ernst
Modular Refinement for Submachines of ASMs. ABZ 2014: 188-203 - [c51]John Derrick
Quiescent Consistency: Defining and Verifying Relaxed Linearizability. FM 2014: 200-214 - [c50]Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif
A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset. IFM 2014: 357-372 - 2013
- [j24]Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst
Compositional Verification of a Lock-Free Stack with RGITL. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013) - [c49]Jörg Pfähler, Gidon Ernst
Formal Specification of an Erase Block Management Layer for Flash Memory. Haifa Verification Conference 2013: 214-229 - [c48]Gidon Ernst
Verification of a Virtual Filesystem Switch. VSTTE 2013: 242-261 - 2012
- [j23]Oleg Travkin, Heike Wehrheim, Gerhard Schellhorn:
Proving Linearizability of Multiset with Local Proof Obligations. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012) - [c47]Gerhard Schellhorn, Heike Wehrheim, John Derrick
How to Prove Algorithms Linearisable. CAV 2012: 243-259 - [c46]Gidon Ernst
A Formal Model of a Virtual Filesystem Switch. SSV 2012: 33-45 - 2011
- [j22]Simon Bäumler, Gerhard Schellhorn, Bogdan Tofan, Wolfgang Reif
Proving linearizability with temporal logic. Formal Aspects Comput. 23(1): 91-112 (2011) - [j21]Dominik Haneberg, Nina Moebius, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel:
Mondex: Engineering a Provable Secure Electronic Purse. Int. J. Softw. Informatics 5(1-2): 159-184 (2011) - [j20]Eerke A. Boiten
Selected papers of the Refinement Workshop Turku (2008). Sci. Comput. Program. 76(9): 737-738 (2011) - [j19]Gerhard Schellhorn:
Completeness of fair ASM refinement. Sci. Comput. Program. 76(9): 756-773 (2011) - [j18]John Derrick
Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1): 4:1-4:43 (2011) - [c45]John Derrick
Verifying Linearisability with Potential Linearisation Points. FM 2011: 323-337 - [c44]Thorsten Bormer, Marc Brockschmidt, Dino Distefano, Gidon Ernst
The COST IC0701 Verification Competition 2011. FoVeOOS 2011: 3-21 - [c43]Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst
Simulating a Flash File System with CoreASM and Eclipse. GI-Jahrestagung 2011: 355 - [c42]Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif
Formal Verification of a Lock-Free Stack with Hazard Pointers. ICTAC 2011: 239-255 - [c41]Gidon Ernst
Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving. SEFM 2011: 188-203 - [c40]Gerhard Schellhorn:
Extending ITL with Interleaved Programs for Interactive Verification. TIME 2011: 7 - [c39]Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst
Interleaved Programs and Rely-Guarantee Reasoning with ITL. TIME 2011: 99-106 - 2010
- [j17]Simon Bäumler, Michael Balser, Florian Nafz
Interactive verification of concurrent systems using symbolic execution. AI Commun. 23(2-3): 285-307 (2010) - [j16]Richard Banach, Gerhard Schellhorn:
Atomic actions, and their refinements to isolated protocols. Formal Aspects Comput. 22(1): 33-61 (2010) - [j15]Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
Automated Flaw Detection in Algebraic Specifications. J. Autom. Reason. 45(4): 359-395 (2010) - [c38]Bogdan Tofan, Simon Bäumler, Gerhard Schellhorn, Wolfgang Reif
Temporal Logic Verification of Lock-Freedom. MPC 2010: 377-396
2000 – 2009
- 2009
- [j14]Eerke A. Boiten
Relational concurrent refinement part II: Internal operations and outputs. Formal Aspects Comput. 21(1-2): 65-102 (2009) - [c37]Gerhard Schellhorn, Simon Bäumler:
Formal Verification of Lock-Free Algorithms. ACSD 2009: 13-18 - [c36]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: 93-110 - [c35]Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
Abstract Specification of the UBIFS File System for Flash Memory. FM 2009: 190-206 - 2008
- [j13]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): 41-59 (2008) - [j12]Gerhard Schellhorn:
ASM Refinement Preserving Invariants. J. Univers. Comput. Sci. 14(12): 1929-1948 (2008) - [c34]Gerhard Schellhorn:
Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract). ABZ 2008: 39-41 - [c33]Gerhard Schellhorn, Richard Banach:
A Concept-Driven Construction of the Mondex Protocol Using Three Refinements. ABZ 2008: 57-70 - [c32]Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif:
Automating Algebraic Specifications of Non-freely Generated Data Types. ATVA 2008: 141-155 - [c31]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: 165-180 - [c30]John Derrick
Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack. FMOODS 2008: 78-95 - [c29]Michael Balser, Simon Bäumler, Wolfgang Reif, Gerhard Schellhorn:
Interactive Verification of Concurrent Systems using Symbolic Execution. LPAR Workshops 2008 - [c28]Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
Bounded Relational Analysis of Free Data Types. TAP 2008: 99-115 - [c27]Eerke A. Boiten
Preface. Refine@FM 2008: 1 - [c26]Gerhard Schellhorn:
Completeness of ASM Refinement. Refine@FM 2008: 25-49 - [e1]Eerke A. Boiten, John Derrick, Gerhard Schellhorn:
Proceedings of the 13th BAC-FACS Refinement Workshop, Refine@FM 2008, Turku, Finland, May 27, 2008. Electronic Notes in Theoretical Computer Science 214, Elsevier 2008 [contents] - 2007
- [c25]Nina Moebius, Dominik Haneberg, Wolfgang Reif
A Modeling Framework for the Development of Provably Secure E-Commerce Applications. ICSEA 2007: 8 - [c24]John Derrick, Gerhard Schellhorn, Heike Wehrheim:
Proving Linearizability Via Non-atomic Refinement. IFM 2007: 195-214 - [c23]Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn:
Verifying Smart Card Applications: An ASM Approach. IFM 2007: 313-332 - [c22]Richard Banach, Gerhard Schellhorn:
On the Refinement of Atomic Actions. REFINE@IFM 2007: 3-30 - 2006
- [c21]Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif:
The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. FM 2006: 16-31 - [c20]Frank Ortmeier, Gerhard Schellhorn:
Formal Fault Tree Analysis - Practical Experiences. AVoCS 2006: 139-151 - 2005
- [j11]Gerhard Schellhorn:
ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor. Comput. Sci. 336(2-3): 403-435 (2005) - [c19]Gerhard Schellhorn:
ASMs and Refinement of State-based Systems. Abstract State Machines 2005: 74-75 - [c18]Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn:
Verifying Security Protocols: An ASM Approach. Abstract State Machines 2005: 247-262 - [c17]Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn:
Formal Safety Analysis of a Radio-Based Railroad Crossing Using Deductive Cause-Consequence Analysis (DCCA). EDCC 2005: 210-224 - 2004
- [c16]Andreas Thums, Gerhard Schellhorn, Frank Ortmeier, Wolfgang Reif:
Interactive Verification of Statecharts. SoftSpez Final Report 2004: 355-373 - [c15]Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn:
Introduction to Subject Area "Verification". SoftSpez Final Report 2004: 419-422 - [c14]Frank Ortmeier, Andreas Thums, Gerhard Schellhorn, Wolfgang Reif:
Combining Formal Methods and Safety Analysis - The ForMoSA Approach. SoftSpez Final Report 2004: 474-493 - [c13]Wolfgang Reif, Frank Ortmeier, Andreas Thums, Gerhard Schellhorn:
Integrated formal methods for safety analysis of train systems. IFIP Congress Topical Sessions 2004: 637-642 - 2003
- [j10]Rudolf Berghammer, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn:
Special Issue on Tools for System Design and Verification. J. Univers. Comput. Sci. 9(2): 86-87 (2003) - [j9]Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif
Safety analysis of the height control system for the Elbtunnel. Reliab. Eng. Syst. Saf. 81(3): 259-268 (2003) - [c12]Andreas Thums, Gerhard Schellhorn:
Model Checking FTA. FME 2003: 739-757 - 2002
- [j8]Gerhard Schellhorn, Wolfgang Reif
Verified Formal Security Models for Multiapplicative Smart Cards. J. Comput. Secur. 10(4): 339-368 (2002) - [j7]Michael Balser, Christoph Duelli, Wolfgang Reif
Verifying Concurrent Systems with Symbolic Execution. J. Log. Comput. 12(4): 549-560 (2002) - [c11]Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering, Helmut Trappschuh:
Safety Analysis of the Height Control System for the Elbtunnel. SAFECOMP 2002: 296-308 - 2001
- [j6]Wolfgang Reif, Gerhard Schellhorn:
J.UCS Special Issue on Tools for System Design and Verification - Part 1. J. Univers. Comput. Sci. 7(1): 1-2 (2001) - [j5]Wolfgang Reif, Gerhard Schellhorn:
J.UCS Special Issue on Tools for System Design and Verification - Part 2. J. Univers. Comput. Sci. 7(2): 105-106 (2001) - [j4]Wolfgang Reif, Gerhard Schellhorn, Tobias Vollmer, Jürgen Ruf:
Correctness of Efficient Real-Time Model Checking. J. Univers. Comput. Sci. 7(2): 194-209 (2001) - [j3]Gerhard Schellhorn:
Verification of ASM Refinements Using Generalized Forward Simulation. J. Univers. Comput. Sci. 7(11): 952-979 (2001) - [c10]Wolfgang Reif, Gerhard Schellhorn, Andreas Thums:
Flaw Detection in Formal Specifications. IJCAR 2001: 642-657 - 2000
- [c9]Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul A. Karger, Vernon Austel, David C. Toll:
Verification of a Formal Security Model for Multiapplicative Smart Cards. ESORICS 2000: 17-36 - [c8]Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Andreas Thums:
Formal System Development with KIV. FASE 2000: 363-366 - [c7]Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn, Tobias Vollmer:
Do You Trust Your Model Checker? FMCAD 2000: 179-196
1990 – 1999
- 1999
- [b1]Gerhard Schellhorn:
Verifikation abstrakter Zustandsmaschinen. University of Ulm, Germany, 1999 - 1998
- [c6]Michael Balser, Wolfgang Reif
KIV 3.0 for Provably Correct Systems. FM-Trends 1998: 330-337 - [c5]Dieter Hutter
VSE: Controlling the Complexity in Formal Software Developments. FM-Trends 1998: 351-358 - 1997
- [j2]Gerhard Schellhorn, Wolfgang Ahrendt:
Reasoning about Abstract State Machines: The WAM Case Study. J. Univers. Comput. Sci. 3(4): 377-413 (1997) - [c4]Wolfgang Reif
Proving System Correctness with KIV 3.0. CADE 1997: 69-72 - [c3]Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel:
Proving System Correctness with KIV. TAPSOFT 1997: 859-862 - 1995
- [p2]Gerhard Schellhorn, Axel Burandt:
KIV. Formal Development of Reactive Systems 1995: 229-245 - [p1]Thomas Fuchß, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel:
Three Selected Case Studies in Verification. KORSO Book 1995: 371-387 - 1994
- [j1]Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel:
Tactics in KIV. J. Inf. Process. Cybern. 30(5/6): 293-310 (1994) - [c2]Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel:
Formal Specification and Verification Using KIV. FTRTFT 1994: 787 - 1993
- [c1]Rainer Drexler, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Werner Stephan, Andreas Wolpers:
The KIV System: A Tool for Formal Program Development. STACS 1993: 704-705
Coauthor Index
[j36] [c73] [c71] [c70] [j35] [c69] [c67] [c66] [c64] [c62] [j31] [c59] [j30] [c58] [j29] [j28] [c54] [p3] [j27] [c53] [c52] [c50] [j24] [c49] [c48] [c46] [j22] [j21] [c43] [c42] [c41] [c39] [j17] [j15] [c38] [c36] [c35] [j13] [c32] [c31] [c29] [c28] [c25] [c23] [c21] [c18] [c17] [c16] [c15] [c14] [c13] [j10] [j9] [j8] [j7] [c11] [j6] [j5] [j4] [c10] [c9] [c8] [c7] [c6] [c5] [c4] [c3] [p1] [j1] [c2] [c1]
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 20:51 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: