Proving linearizability with temporal logic

DOI10.1007/s00165-009-0130-yzbMath1214.68209OpenAlexW2103524479MaRDI QIDQ539223

Gerhard Schellhorn, Simon Bäumler, Bogdan Tofan, Wolfgang Reif

Publication date: 27 May 2011

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://opus.bibliothek.uni-augsburg.de/opus4/files/1214/TR_2008_19.pdf

zbMATH Keywords

verificationtemporal logiclinearizabilitycompositional reasoninglock-freerely-guarantee

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (6)

An application of temporal projection to interleaving concurrency ⋮ Interconnections between classes of sequentially compositional temporal formulas ⋮ Guest editors' preface to special issue on interval temporal logics ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Compositional reasoning using intervals and time reversal ⋮ Formal Verification of a Lock-Free Stack with Hazard Pointers

Uses Software

• Isabelle
• TLPVS
• KIV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A scalable lock-free stack algorithm
• Assumption/guarantee specifications in linear-time temporal logic
• Lock-free parallel and concurrent garbage collection by mark\&sweep
• Trace-based derivation of a scalable lock-free stack algorithm
• Recognizing safety and liveness
• Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
• Refinement verification of the lazy caching algorithm
• Thread Quantification for Concurrent Shape Analysis
• A Marriage of Rely/Guarantee and Separation Logic
• Interactive verification of concurrent systems using symbolic execution
• Shape-Value Abstraction for Verifying Linearizability
• Proving Linearizability Via Non-atomic Refinement
• Modular Safety Checking for Fine-Grained Concurrency
• Tentative steps toward a development method for interfering programs
• Abstract State Machines
• Evolving Algebras 1993: Lipari Guide
• Comparison Under Abstraction for Verifying Linearizability
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Proving linearizability with temporal logic