Wait-free linearization with a mechanical proof

DOI10.1007/BF01784240zbMath1448.68110OpenAlexW2169164504MaRDI QIDQ5137000

Wim H. Hesselink

Publication date: 30 November 2020

Published in: Distributed Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01784240

zbMATH Keywords

correctnessmemory managementconsensuswait-freemechanical verificationlinearizableBoyer-Moore logicgrain of atomicityshared data object

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14) Distributed algorithms (68W15)

Related Items

Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos

Uses Software

• HOL
• NQTHM
• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A calculus of communicating systems
• A verification system for concurrent programs based on the Boyer-Moore prover
• Beyond atomic registers: Bounded wait-free implementations of nontrivial objects
• An axiomatic proof technique for parallel programs
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• FM8501: a verified microprocessor
• Applications of Process Algebra
• Wait-free linearization with an assertional proof