Formal Verification of a Lock-Free Stack with Hazard Pointers

DOI10.1007/978-3-642-23283-1_16zbMath1350.68081OpenAlexW2108915642MaRDI QIDQ3105753

Bogdan Tofan, Gerhard Schellhorn, Wolfgang Reif

Publication date: 6 January 2012

Published in: Theoretical Aspects of Computing – ICTAC 2011 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-23283-1_16

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) Data structures (68P05)

Related Items (3)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Formal Verification of a Lock-Free Stack with Hazard Pointers

Uses Software

• KIV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving linearizability with temporal logic
• Formal Verification of a Lock-Free Stack with Hazard Pointers
• Modular verification of a non-blocking stack
• Interactive verification of concurrent systems using symbolic execution
• Temporal Logic Verification of Lock-Freedom
• Reasoning about Optimistic Concurrency Using a Program Logic for History
• Formal Techniques for Networked and Distributed Systems – FORTE 2004

This page was built for publication: Formal Verification of a Lock-Free Stack with Hazard Pointers