Skip to content

Gerhard Schellhorn

Publication record assembled from the DBLP archive of ranked conferences.

Papers indexed

43

Venues

23

Active years

1993–2025

Best venue rank

A*

Where they publish

Papers

43 indexed papers, newest first.

YearVenueTitleAuthors
2025IFMModel Checking Buffered Durable Linearizability in CSP.Chelsea Edmonds, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2024IFMVeriCode: Correct Translation of Abstract Specifications to C Code.Gerhard Schellhorn, Stefan Bodenmller, Wolfgang Reif
2024VMCAIA Fully Verified Persistency Library.Stefan Bodenmller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2023IFMRefinement and Separation: Modular Verification of Wandering Trees.Gerhard Schellhorn, Stefan Bodenmller, Wolfgang Reif
2022CONCURWeak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement.Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2020FORTEDefining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory.Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
2020IFMModular Integration of Crashsafe Caching into a Verified Virtual File System Switch.Stefan Bodenmller, Gerhard Schellhorn, Wolfgang Reif
2019FMVerifying Correctness of Persistent Concurrent Data Structures.John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim
2018SEFMFastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity.Gerhard Schellhorn, Monika Wedel, Oleg Travkin, Jrgen Knig, Heike Wehrheim
2017IFMModular Verification of Order-Preserving Write-Back Caches.Jrg Pfhler, Gidon Ernst, Stefan Bodenmller, Gerhard Schellhorn, Wolfgang Reif
2016IFMTowards a Thread-Local Proof Technique for Starvation Freedom.Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
2016OPODISProving Opacity of a Pessimistic STM.Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
2015FMVerifying Opacity of a Transactional Mutex Lock.John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
2014FMQuiescent Consistency: Defining and Verifying Relaxed Linearizability.John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim
2014IFMA Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset.Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif
2012CAVHow to Prove Algorithms Linearisable.Gerhard Schellhorn, Heike Wehrheim, John Derrick
2011FMVerifying Linearisability with Potential Linearisation Points.John Derrick, Gerhard Schellhorn, Heike Wehrheim
2011GISimulating a Flash File System with CoreASM and Eclipse.Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst
2011ICTACFormal Verification of a Lock-Free Stack with Hazard Pointers.Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif
2011SEFMVerification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving.Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
2011TIMEExtending ITL with Interleaved Programs for Interactive Verification.Gerhard Schellhorn
2011TIMEInterleaved Programs and Rely-Guarantee Reasoning with ITL.Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Wolfgang Reif
2010MPCTemporal Logic Verification of Lock-Freedom.Bogdan Tofan, Simon Bumler, Gerhard Schellhorn, Wolfgang Reif
2009FMAbstract Specification of the UBIFS File System for Flash Memory.Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
2008ATVAAutomating Algebraic Specifications of Non-freely Generated Data Types.Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
2008FMVerification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code.Holger Grandy, Markus Bischof, Kurt Stenzel, Gerhard Schellhorn, Wolfgang Reif
2008LPARInteractive Verification of Concurrent Systems using Symbolic Execution.Michael Balser, Simon Bumler, Wolfgang Reif, Gerhard Schellhorn
2008TAPBounded Relational Analysis of Free Data Types.Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif
2007ICSEAA Modeling Framework for the Development of Provably Secure E-Commerce Applications.Nina Moebius, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn
2007IFMProving Linearizability Via Non-atomic Refinement.John Derrick, Gerhard Schellhorn, Heike Wehrheim
2007IFMVerifying Smart Card Applications: An ASM Approach.Dominik Haneberg, Holger Grandy, Wolfgang Reif, Gerhard Schellhorn
2006FMThe Mondex Challenge: Machine Checked Proofs for an Electronic Purse.Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif
2005EDCCFormal Safety Analysis of a Radio-Based Railroad Crossing Using Deductive Cause-Consequence Analysis (DCCA).Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn
2003FMModel Checking FTA.Andreas Thums, Gerhard Schellhorn
2002SAFECOMPSafety Analysis of the Height Control System for the Elbtunnel.Frank Ortmeier, Gerhard Schellhorn, Andreas Thums, Wolfgang Reif, Bernhard Hering, Helmut Trappschuh
2001CADEFlaw Detection in Formal Specifications.Wolfgang Reif, Gerhard Schellhorn, Andreas Thums
2000ESORICSVerification of a Formal Security Model for Multiapplicative Smart Cards.Gerhard Schellhorn, Wolfgang Reif, Axel Schairer, Paul A. Karger, Vernon Austel, David C. Toll
2000FASEFormal System Development with KIV.Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Andreas Thums
2000FMCADDo You Trust Your Model Checker?Wolfgang Reif, Jrgen Ruf, Gerhard Schellhorn, Tobias Vollmer
1998FMKIV 3.0 for Provably Correct Systems.Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1998FMVSE: 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
1997CADEProving System Correctness with KIV 3.0.Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel
1993STACSThe KIV System: A Tool for Formal Program Development.Rainer Drexler, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Werner Stephan, Andreas Wolpers