Model Checking Simulation Rules for Linearizability

DOI10.1007/978-3-319-41591-8_13zbMath1390.68439OpenAlexW2484472566MaRDI QIDQ4571132

Graeme Smith

Publication date: 6 July 2018

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-41591-8_13

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)

Uses Software

• SPIN
• TLC
• Z

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying data refinements using a model checker
• Model checking action system refinements
• Concurrent Library Correctness on the TSO Memory Model
• A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
• Modular Safety Checking for Fine-Grained Concurrency
• Show No Weakness: Sequentially Consistent Specifications of TSO Libraries
• Computer Aided Verification
• Comparison Under Abstraction for Verifying Linearizability
• Formal Techniques for Networked and Distributed Systems – FORTE 2004

This page was built for publication: Model Checking Simulation Rules for Linearizability