Gerhard Schellhorn

Available identifiers

zbMath Open schellhorn.gerhardMaRDI QIDQ539220

List of research outcomes

Publication	Date of Publication	Type
Weak progressive forward simulation is necessary and sufficient for strong observational refinement	2024-08-13	Paper
Verifying correctness of persistent concurrent data structures	2024-03-14	Paper
https://portal.mardi4nfdi.de/entity/Q6083440	2023-12-08	Paper
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory	2022-10-13	Paper
https://portal.mardi4nfdi.de/entity/Q5101340	2022-08-30	Paper
Flashix: modular verification of a concurrent and crash-safe flash file system	2022-03-22	Paper
Verifying correctness of persistent concurrent data structures: a sound and complete method	2021-09-14	Paper
Verifying Opacity of a Transactional Mutex Lock	2019-12-19	Paper
Mechanized proofs of opacity: a comparison of two techniques	2018-09-12	Paper
Proving Opacity of a Pessimistic {STM}	2018-07-18	Paper
Towards a Thread-Local Proof Technique for Starvation Freedom	2016-06-17	Paper
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures	2015-09-17	Paper
Formal Fault Tree Analysis - Practical Experiences	2015-03-18	Paper
RGITL: a temporal logic framework for compositional reasoning about interleaved programs	2014-07-11	Paper
Completeness of ASM Refinement	2014-03-26	Paper
Formal Verification of a Lock-Free Stack with Hazard Pointers	2012-01-06	Paper
Completeness of fair ASM refinement	2011-06-06	Paper
Proving linearizability with temporal logic	2011-05-27	Paper
Automated flaw detection in algebraic specifications	2011-01-12	Paper
Temporal Logic Verification of Lock-Freedom	2010-07-26	Paper
Interactive verification of concurrent systems using symbolic execution	2010-06-17	Paper
Atomic actions, and their refinements to isolated protocols	2010-03-08	Paper
Relational concurrent refinement. II: Internal operations and outputs	2009-05-27	Paper
Proving Linearizability Via Non-atomic Refinement	2009-03-06	Paper
Automating Algebraic Specifications of Non-freely Generated Data Types	2008-11-20	Paper
https://portal.mardi4nfdi.de/entity/Q3539946	2008-11-19	Paper
Bounded Relational Analysis of Free Data Types	2008-04-24	Paper
ASM refinement and generalizations of forward simulation in data refinement: a comparison	2005-06-10	Paper
Verifying Concurrent Systems with Symbolic Execution	2002-09-11	Paper
https://portal.mardi4nfdi.de/entity/Q4539647	2002-07-10	Paper
The WAM case study: Verifying compiler correctness for Prolog with KIV	2002-01-21	Paper
Theorem proving in large theories	2001-11-06	Paper
Correctness of efficient real-time model checking	2001-08-13	Paper
https://portal.mardi4nfdi.de/entity/Q4520493	2001-02-26	Paper
https://portal.mardi4nfdi.de/entity/Q4524764	2001-01-15	Paper
https://portal.mardi4nfdi.de/entity/Q4524769	2001-01-15	Paper
https://portal.mardi4nfdi.de/entity/Q4858951	1995-12-20	Paper
https://portal.mardi4nfdi.de/entity/Q4281573	1995-11-23	Paper

Research outcomes over time

This page was built for person: Gerhard Schellhorn