Proving linearizability with temporal logic
type: Item
instance of: scholarly article
title: Proving linearizability with temporal logic
zbMATH Open document ID: 1214.68209
author: Simon Bäumler
author: Gerhard Schellhorn
author: Bogdan Tofan
author: Wolfgang Reif
published in: Formal Aspects of Computing
publication date: 2011-05-27T00:00:00Z
full work available at URL: TR 2008 19.pdf
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 5900644
zbMATH Keywords: lock-free
zbMATH Keywords: linearizability
zbMATH Keywords: verification
zbMATH Keywords: temporal logic
zbMATH Keywords: compositional reasoning
zbMATH Keywords: rely-guarantee
describes a project that uses: TLPVS
describes a project that uses: Isabelle
describes a project that uses: KIV
MaRDI profile type: Publication
OpenAlex ID: W2103524479
cites work: Comparison Under Abstraction for Verifying Linearizability
cites work: Recognizing safety and liveness
cites work: Q5291078
cites work: Interactive verification of concurrent systems using symbolic execution
cites work: Thread Quantification for Concurrent Shape Analysis
cites work: Abstract State Machines
cites work: Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
cites work: Verifying concurrent data structures by simulation
cites work: Modular Safety Checking for Fine-Grained Concurrency
cites work: Formal Techniques for Networked and Distributed Systems – FORTE 2004
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Concurrency verification. Introduction to compositional and noncompositional methods
cites work: Proving Linearizability Via Non-atomic Refinement
cites work: Trace-based derivation of a scalable lock-free stack algorithm
cites work: Lock-free parallel and concurrent garbage collection by mark\&sweep
cites work: Evolving Algebras 1993: Lipari Guide
cites work: Q4343990
cites work: Refinement verification of the lazy caching algorithm
cites work: A scalable lock-free stack algorithm
cites work: Tentative steps toward a development method for interfering programs
cites work: Assumption/guarantee specifications in linear-time temporal logic
cites work: Q3024875
cites work: Q3680239
cites work: Q4417904
cites work: Q4524764
cites work: Shape-Value Abstraction for Verifying Linearizability
cites work: A Marriage of Rely/Guarantee and Separation Logic
Wikidata QID: Q130880043
DOI: 10.1007/S00165-009-0130-Y
description: scientific article; zbMATH DE number 5900644