Gerhard Schellhorn

According to our database1, Gerhard Schellhorn authored at least 95 papers between 1993 and 2018.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2018
Symbolic execution for a clash-free subset of ASMs.
Sci. Comput. Program., 2018

Mechanized proofs of opacity: a comparison of two techniques.
Formal Asp. Comput., 2018

FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity.
Proceedings of the Software Engineering and Formal Methods - 16th International Conference, 2018

2017
Modular Verification of Order-Preserving Write-Back Caches.
Proceedings of the Integrated Formal Methods - 13th International Conference, 2017

2016
Modular, crash-safe refinement for ASMs with submachines.
Sci. Comput. Program., 2016

Proving Opacity of a Pessimistic STM.
Proceedings of the 20th International Conference on Principles of Distributed Systems, 2016

Towards a Thread-Local Proof Technique for Starvation Freedom.
Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

A Relational Encoding for a Clash-Free Subset of ASMs.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

2015
KIV: overview and VerifyThis competition.
STTT, 2015

Verification of B+ trees by integration of shape analysis and interactive theorem proving.
Software and System Modeling, 2015

Inside a Verified Flash File System: Transactions and Garbage Collection.
Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Verifying Opacity of a Transactional Mutex Lock.
Proceedings of the FM 2015: Formal Methods, 2015

Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications.
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.
ACM Trans. Comput. Log., 2014

Two approaches for proving linearizability of multiset.
Sci. Comput. Program., 2014

RGITL: A temporal logic framework for compositional reasoning about interleaved programs.
Ann. Math. Artif. Intell., 2014

A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset.
Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Quiescent Consistency: Defining and Verifying Relaxed Linearizability.
Proceedings of the FM 2014: Formal Methods, 2014

Development of a Verified Flash File System.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

Modular Refinement for Submachines of ASMs.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013
Compositional Verification of a Lock-Free Stack with RGITL.
ECEASST, 2013

Verification of a Virtual Filesystem Switch.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Formal Specification of an Erase Block Management Layer for Flash Memory.
Proceedings of the Hardware and Software: Verification and Testing, 2013

2012
Proving Linearizability of Multiset with Local Proof Obligations.
ECEASST, 2012

A Formal Model of a Virtual Filesystem Switch
Proceedings of the Proceedings Seventh Conference on Systems Software Verification, 2012

How to Prove Algorithms Linearisable.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Mechanically verified proof obligations for linearizability.
ACM Trans. Program. Lang. Syst., 2011

Completeness of fair ASM refinement.
Sci. Comput. Program., 2011

Selected papers of the Refinement Workshop Turku (2008).
Sci. Comput. Program., 2011

Mondex: Engineering a Provable Secure Electronic Purse.
Int. J. Software and Informatics, 2011

Proving linearizability with temporal logic.
Formal Asp. Comput., 2011

Interleaved Programs and Rely-Guarantee Reasoning with ITL.
Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Extending ITL with Interleaved Programs for Interactive Verification.
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.
Proceedings of the Software Engineering and Formal Methods - 9th International Conference, 2011

Formal Verification of a Lock-Free Stack with Hazard Pointers.
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.
Proceedings of the Informatik 2011: Informatik schafft Communities, 2011


Verifying Linearisability with Potential Linearisation Points.
Proceedings of the FM 2011: Formal Methods, 2011

2010
Automated Flaw Detection in Algebraic Specifications.
J. Autom. Reasoning, 2010

Atomic actions, and their refinements to isolated protocols.
Formal Asp. Comput., 2010

Interactive verification of concurrent systems using symbolic execution.
AI Commun., 2010

Temporal Logic Verification of Lock-Freedom.
Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010

2009
Relational concurrent refinement part II: Internal operations and outputs.
Formal Asp. Comput., 2009

Abstract Specification of the UBIFS File System for Flash Memory.
Proceedings of the FM 2009: Formal Methods, 2009

A Systematic Verification Approach for Mondex Electronic Purses Using ASMs.
Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009

Formal Verification of Lock-Free Algorithms.
Proceedings of the Ninth International Conference on Application of Concurrency to System Design, 2009

2008
ASM Refinement Preserving Invariants.
J. UCS, 2008

Verification of Mondex electronic purses with KIV: from transactions to a security protocol.
Formal Asp. Comput., 2008

Completeness of ASM Refinement.
Electr. Notes Theor. Comput. Sci., 2008

Preface.
Electr. Notes Theor. Comput. Sci., 2008

On the Refinement of Atomic Actions.
Electr. Notes Theor. Comput. Sci., 2008

Bounded Relational Analysis of Free Data Types.
Proceedings of the Tests and Proofs, Second International Conference, 2008

Interactive Verification of Concurrent Systems using Symbolic Execution.
Proceedings of the LPAR 2008 Workshops, 2008

Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack.
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.
Proceedings of the FM 2008: Formal Methods, 2008

Automating Algebraic Specifications of Non-freely Generated Data Types.
Proceedings of the Automated Technology for Verification and Analysis, 2008

A Concept-Driven Construction of the Mondex Protocol Using Three Refinements.
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

Refinement of State-Based Systems: ASMs and Big Commuting Diagrams (Abstract).
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2007
Formal Fault Tree Analysis - Practical Experiences.
Electr. Notes Theor. Comput. Sci., 2007

Verifying Smart Card Applications: An ASM Approach.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Proving Linearizability Via Non-atomic Refinement.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

A Modeling Framework for the Development of Provably Secure E-Commerce Applications.
Proceedings of the Second International Conference on Software Engineering Advances (ICSEA 2007), 2007

2006
The Mondex Challenge: Machine Checked Proofs for an Electronic Purse.
Proceedings of the FM 2006: Formal Methods, 2006

2005
ASM refinement and generalizations of forward simulation in data refinement: a comparison.
Theor. Comput. Sci., 2005

Formal Safety Analysis of a Radio-Based Railroad Crossing Using Deductive Cause-Consequence Analysis (DCCA).
Proceedings of the Dependable Computing, 2005

ASMs and Refinement of State-based Systems.
Proceedings of the 12th International Workshop on Abstract State Machines, 2005

Verifying Security Protocols: An ASM Approach.
Proceedings of the 12th International Workshop on Abstract State Machines, 2005

2004
Integrated formal methods for safety analysis of train systems.
Proceedings of the Building the Information Society, 2004

Interactive Verification of Statecharts.
Proceedings of the Integration of Software Specification Techniques for Applications in Engineering, 2004

Combining Formal Methods and Safety Analysis - The ForMoSA Approach.
Proceedings of the Integration of Software Specification Techniques for Applications in Engineering, 2004

Introduction to Subject Area "Verification".
Proceedings of the Integration of Software Specification Techniques for Applications in Engineering, 2004

2003
Special Issue on Tools for System Design and Verification.
J. UCS, 2003

Model Checking FTA.
Proceedings of the FME 2003: Formal Methods, 2003

2002
Verifying Concurrent Systems with Symbolic Execution.
J. Log. Comput., 2002

Verified Formal Security Models for Multiapplicative Smart Cards.
Journal of Computer Security, 2002

Safety Analysis of the Height Control System for the Elbtunnel.
Proceedings of the Computer Safety, 2002

2001
Verification of ASM Refinements Using Generalized Forward Simulation.
J. UCS, 2001

Correctness of Efficient Real-Time Model Checking.
J. UCS, 2001

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

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

Flaw Detection in Formal Specifications.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000
Do You Trust Your Model Checker?
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Formal System Development with KIV.
Proceedings of the Fundamental Approaches to Software Engineering, 2000

Verification of a Formal Security Model for Multiapplicative Smart Cards.
Proceedings of the Computer Security, 2000

1999
Verifikation abstrakter Zustandsmaschinen.
PhD thesis, 1999

1998
VSE: Controlling the Complexity in Formal Software Developments.
Proceedings of the Applied Formal Methods, 1998

KIV 3.0 for Provably Correct Systems.
Proceedings of the Applied Formal Methods, 1998

1997
Reasoning about Abstract State Machines: The WAM Case Study.
J. UCS, 1997

Proving System Correctness with KIV.
Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

Proving System Correctness with KIV 3.0.
Proceedings of the Automated Deduction, 1997

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

Three Selected Case Studies in Verification.
Proceedings of the KORSO, 1995

1994
Tactics in KIV.
Elektronische Informationsverarbeitung und Kybernetik, 1994

Formal Specification and Verification Using KIV.
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.
Proceedings of the STACS 93, 1993


  Loading...